Model Checking UML Activity Diagrams with SPIN

Author

Li Jing ; Li Jinhua ; Zhang Fangning

Author_Institution

Coll. of Inf. Eng., Qingdao Univ., Qingdao, China

fYear

2009

fDate

11-13 Dec. 2009

Firstpage

1

Lastpage

4

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/CISE.2009.5363181

Filename

5363181