Verifying UML-based interaction using coloured Petri nets

Aditya Bagoes Saputa; Thomas Anung Basuki; Jimmy Tirtawangsa

doi:10.1109/ICODSE.2014.7062709

Verifying UML-based interaction using coloured Petri nets

Aditya Bagoes Saputa
, Thomas Anung Basuki
, Jimmy Tirtawangsa

School of Mathematical & Computer Sciences

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	2014 International Conference on Data and Software Engineering (ICODSE)
Publisher	IEEE
ISBN (Electronic)	9781479979967
DOIs	https://doi.org/10.1109/ICODSE.2014.7062709
Publication status	Published - 19 Mar 2015
Event	2014 International Conference on Data and Software Engineering - Bandung, Indonesia Duration: 26 Nov 2014 → 27 Nov 2014

Conference

Conference	2014 International Conference on Data and Software Engineering
Abbreviated title	ICODSE 2014
Country/Territory	Indonesia
City	Bandung
Period	26/11/14 → 27/11/14

Keywords

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

ASJC Scopus subject areas

Software
Information Systems

Access to Document

10.1109/ICODSE.2014.7062709

Cite this

@inproceedings{87b07929eaff46a6b3720a7c63ca0244,

title = "Verifying UML-based interaction using coloured Petri nets",

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 = "CPN, fairness, liveness, model-checking, sequence diagram, state space, UML, verification",

author = "Saputa, \{Aditya Bagoes\} and Basuki, \{Thomas Anung\} and Jimmy Tirtawangsa",

note = "Publisher Copyright: {\textcopyright} 2014 IEEE.; 2014 International Conference on Data and Software Engineering, ICODSE 2014 ; Conference date: 26-11-2014 Through 27-11-2014",

year = "2015",

month = mar,

day = "19",

doi = "10.1109/ICODSE.2014.7062709",

language = "English",

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

publisher = "IEEE",

address = "United States",

}

TY - GEN

T1 - Verifying UML-based interaction using coloured Petri nets

AU - Saputa, Aditya Bagoes

AU - Basuki, Thomas Anung

AU - Tirtawangsa, Jimmy

PY - 2015/3/19

Y1 - 2015/3/19

N2 - 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.

AB - 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.

KW - CPN

KW - fairness

KW - liveness

KW - model-checking

KW - sequence diagram

KW - state space

KW - UML

KW - verification

UR - https://www.scopus.com/pages/publications/84946685347

U2 - 10.1109/ICODSE.2014.7062709

DO - 10.1109/ICODSE.2014.7062709

M3 - Conference contribution

AN - SCOPUS:84946685347

BT - 2014 International Conference on Data and Software Engineering (ICODSE)

PB - IEEE

T2 - 2014 International Conference on Data and Software Engineering

Y2 - 26 November 2014 through 27 November 2014

ER -

Verifying UML-based interaction using coloured Petri nets

Abstract

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this