Title :
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
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;
Conference_Titel :
Data and Software Engineering (ICODSE), 2014 International Conference on
Print_ISBN :
978-1-4799-8175-5
DOI :
10.1109/ICODSE.2014.7062709
