From UML 2.0 Sequence Diagrams to PROMELA code by Graph Transformation using AToM3.
Mouna Ait Oubelli, Nadia Younsi, Abdelkrim Amirat, Ahcene Menasria · CIIA · 2011
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, we 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). Graph transformation is used as an approach of model transformation to propose a graph grammar for the translation using AToM3 tool.