From UML 2.0 Sequence Diagrams to PROMELA Code by Graph Transformation Using AToM
Source: Tilburg University
A main challenge in software development process is to bring error detection to first phases of the software life cycle. The Verification and Validation (V&V) of UML diagrams is of interest in a number of applications such as detecting flaws at the design phase for software security, where it is crucial to detect security flaws before they can be exploited. In this paper, the authors propose an approach using a transformation tool to create a PROMELA code based model from UML interactions expressed in sequence diagram to use in SPIN model checker to simulate the execution and to verify properties written in Linear Temporal Logic (LTL).