Model Checking UML Activity Diagrams with SPIN
Jing Li, Jinhua Li, Fangning Zhang · 2009
UML activity diagram describes the software internal activities. It is an important tool to model the dynamic behavior of software systems in the early software development. An approach to finding software vulnerabilities earlier by verifying UML activity diagrams with model checking technique is put forwarded in the paper. Firstly, the UML activity diagrams are converted into extended hierarchical automata (EHA). Then the EHA models are transformed in PROMELA model which is input of SPIN model checker. The correctness of the conversion process is showed in the simulation of the dining-philosophers problem with SPIN.