Formal Verification and Validation of UML 2.0 Sequence Diagrams using Source and Destination of Messages
Why this work is in the frame
A frame that forgets how it found something cannot be audited. These are the routes that admitted this work.
Bibliographic record
Abstract
A major challenge in software development process is to advance error detection to early phases of the software life cycle. For this purpose, the Verification and Validation (V&V) of UML diagrams play a very important role in detecting flaws at the design phase. It has a distinct importance for software security, where it is crucial to detect security flaws before they can be exploited. This paper presents a formal V&V technique for one of the most popular UML diagrams: sequence diagrams. The proposed approach creates a PROMELA-based model from UML interactions expressed in sequence diagrams, and uses SPIN model checker to simulate the execution and to verify properties written in Linear Temporal Logic (LTL). The whole technique is implemented as an Eclipse plugin, which hides the model-checking formalism from the user. The main contribution of this work is to provide an efficient mechanism to be able to track the execution state of an interaction, which allows designers to write relevant properties involving send/receive events and source/destination of messages using LTL. Another important contribution is the definition of the PROMELA structure that provides a precise semantics of most of the newly UML 2.0 introduced combined fragments, allowing the execution of complex interactions. Finally, we illustrate the benefits of our approach through a security-related case study in a real world scenario.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
Full frame distilled prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. Learned from the 10,348 direct Codex labels and 10,348 direct Gemma labels. Candidate is the union of thresholded teacher heads; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels or direct frontier model labels.
Codex and Gemma teacher scores by category
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.003 | 0.000 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.000 | 0.000 |
| Bibliometrics | 0.000 | 0.001 |
| Science and technology studies | 0.000 | 0.001 |
| Scholarly communication | 0.000 | 0.001 |
| Open science | 0.001 | 0.000 |
| Research integrity | 0.000 | 0.000 |
| Insufficient payload (model declined to judge) | 0.000 | 0.000 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from it