Validation environment of UML2 IOD based on hierarchical coloured Petri nets. (6th June 2013)

• Record Type: Journal Article
• Authors: Bennama, Miloud; Bouabana–Tebibel, Thouraya
• Is Part Of: International journal of computer applications technology. Volume 47:Number 2/3(2013)
• Page Start: 227
• Page End: 240
• Publication Date: 2013-06-06
• Subjects: UML2 -- interaction overview diagram -- sequence diagrams -- OCL constraint -- hierarchical coloured Petri nets -- ASKCTL temporal logic formula -- modelling -- semantics -- formalisation -- mapping -- validation -- state space analysis -- simulation -- model checking -- CPNTools -- ATM system; Technology -- Data processing -- Periodicals; 620.00285
• Languages: English
• ISSNs: 0952-8091

Abstract

A new interaction diagram, called Interaction Overview Diagram or IOD, was introduced in the second generation of UML. It defines interactions through a variant of activity diagrams in a way that promotes overview of the control flow. But its semantics remains unclear thus requiring formalisation tasks. We propose in this paper a validation environment for UML IODs. So we first formalise their semantics by translation to the semantics domain of Hierarchical Coloured Petri Nets, or HCPNs for short. The derived HCPN models are afterwards analysed by means of the model–checker CPNtools. The analysis tackles the simulation, verification and validation aspects. It especially focuses on the validation of system properties written by the UML designer. The properties are expressed in OCL and then automatically translated into ASKCTL temporal logic. A case study of an ATM system illustrates the approach.