Authors: Miloud Bennama; Thouraya Bouabana-Tebibel
Addresses: Laboratoire de Communication des Systèmes Informatiques, Ecole nationale Supérieure d'Informatique, BP 68M Oued-Smar, 16309 Alger, Algeria ' Laboratoire de Communication des Systèmes Informatiques, Ecole nationale Supérieure d'Informatique, BP 68M Oued-Smar, 16309 Alger, Algeria
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.
Keywords: 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.
International Journal of Computer Applications in Technology, 2013 Vol.47 No.2/3, pp.227 - 240
Received: 08 May 2021
Accepted: 12 May 2021
Published online: 05 Jun 2013 *