Verifying UML-based interaction using coloured Petri nets

Author

Saputa, Aditya Bagoes ; Basuki, Thomas Anung ; Tirtawangsa, Jimmy

Author_Institution

Dept. of Inf., Parahyangan Catholic Univ., Bandung, Indonesia

fYear

2014

Firstpage

1

Lastpage

6

Abstract

Verification of an interaction design becomes very important in the system development. Meanwhile, UML, as a standard tool in the system development, is not able to provide a formal verification of the design directly. This paper provides an approach to verify the UML-based interaction by using CPN. The interaction is modelled using UML 2.0 sequence diagram. The verification focuses on identifying the reachability, deadlock, inconsistency, and user errors: initialisation error, order error, and post-completion error. This verification uses the CPN analysis techniques such as state space analysis, strongly-connected component graph, liveness properties and fairness properties. Using a case study of chocolate machine, the verification approach is applied.

Keywords

Petri nets; Unified Modeling Language; diagrams; formal verification; CPN analysis techniques; UML 2.0 sequence diagram; UML-based interaction; coloured Petri nets; deadlock; fairness properties; formal verification; inconsistency; initialisation error; interaction design; liveness properties; order error; post-completion error; reachability; state space analysis; strongly-connected component graph; system development; user errors; Analytical models; Color; Firing; Petri nets; System recovery; Transforms; Unified modeling language; CPN; UML; fairness; liveness; model-checking; sequence diagram; state space; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Data and Software Engineering (ICODSE), 2014 International Conference on

Print_ISBN

978-1-4799-8175-5

Type

conf

DOI

10.1109/ICODSE.2014.7062709

Filename

7062709