Title :
Model Checking UML Activity Diagrams with SPIN
Author :
Li Jing ; Li Jinhua ; Zhang Fangning
Author_Institution :
Coll. of Inf. Eng., Qingdao Univ., Qingdao, China
Abstract :
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.
Keywords :
Unified Modeling Language; automata theory; program verification; EHA model; PROMELA model; SPIN model checking; UML activity diagram; dining-philosophers problem; extended hierarchical automata; software development; software internal activity; software system dynamic behavior; software vulnerability; Application software; Automata; Educational institutions; Logic testing; Programming; Security; Software systems; Strontium; System testing; Unified modeling language;
Conference_Titel :
Computational Intelligence and Software Engineering, 2009. CiSE 2009. International Conference on
Conference_Location :
Wuhan
Print_ISBN :
978-1-4244-4507-3
Electronic_ISBN :
978-1-4244-4507-3
DOI :
10.1109/CISE.2009.5363181
