Verifying UML-based Interaction Using Coloured Petri Nets

被引：0

作者：

Saputra, Aditya Bagoes ^{[1
]}

Basuki, Thomas Anung ^{[1
]}

Tirtawangsa, Jimmy ^{[2
]}

机构：

[1] Parahyangan Catholic Univ, Dept Informat, Bandung, Indonesia

[2] Telkom Univ, Sch Comp, Bandung, Indonesia

来源：

2014 International Conference on Data and Software Engineering (ICODSE) | 2014年

关键词：

UML; sequence diagram; verification; CPN; state space; liveness; fairness; model-checking;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页数：6

共 50 条

[1] Verifying Parallel Algorithms and Programs Using Coloured Petri Nets
Westergaard, Michael
TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY VI, 2012, 7400 : 146 - 168
[2] Modeling and Verifying Asynchronous Communication Mechanisms using Coloured Petri Nets
Gorgonio, Kyller
Xia, Fei
2008 8TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2008, : 138 - +
[3] Formalising concurrent UML state machines using coloured Petri nets
Andre, Etienne
Benmoussa, Mohamed Mahdi
Choppy, Christine
FORMAL ASPECTS OF COMPUTING, 2016, 28 (05) : 805 - 845
[4] Transformation of Coloured Petri Nets to UML 2 Diagrams
Yassin, Ayman
Hassan, Hoda
NEW PERSPECTIVES IN INFORMATION SYSTEMS AND TECHNOLOGIES, VOL 2, 2014, 276 : 131 - 142
[5] A Coloured Petri Net formalisation for a UML-based notation applied to cooperative system modelling
Garrido, JL
Gea, M
INTERACTIVE SYSTEMS: DESIGN, SPECIFICATION AND VERIFICATION, 2002, 2545 : 16 - 28
[6] Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report
Andre, Etienne
Mahdi Benmoussa, Mohamed
Choppy, Christine
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (150): : 1 - 7
[7] Transformation of UML 2.0 Sequence Diagram into Coloured Petri Nets
Saputra, Aditya Bagoes
Basuki, Thomas Anung
Tirtawangsa, Jimmy
2014 International Conference of Advanced Informatics: Concept, Theory and Application (ICAICTA), 2014, : 243 - 248
[8] Validation environment of UML2 IOD based on hierarchical coloured Petri nets
Bennama, Miloud
Bouabana-Tebibel, Thouraya
INTERNATIONAL JOURNAL OF COMPUTER APPLICATIONS IN TECHNOLOGY, 2013, 47 (2-3) : 227 - 240
[9] Modeling interaction in cooperative information systems using coloured Petri nets
Camargo-Santacruz, F
Ramos-Quintana, F
Frausto-Solis, J
7TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XII, PROCEEDINGS: INFORMATION SYSTEMS, TECHNOLOGIES AND APPLICATIONS: II, 2003, : 334 - 344
[10] Verifying enterprise's mandatory access control policies with coloured Petri nets
Juszczyszyn, K
TWELFTH IEEE INTERNATIONAL WORKSHOPS ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES, PROCEEDINGS, 2003, : 184 - 189

← 1 2 3 4 5 →