Authors: Thouraya Bouabana-Tebibel; Lila Méziani
Addresses: Laboratoire de Communication des Systèmes Informatiques (LCSI), École Nationale Supérieure d'Informatique (ESI), BP 68 M Oued-Smar, Algiers, Algeria ' Laboratoire de Communication des Systèmes Informatiques (LCSI), École Nationale Supérieure d'Informatique (ESI), BP 68 M Oued-Smar, Algiers, Algeria
Abstract: UML semantics formalisation has aroused much interest these two last decades. Among the numerous proposed works many undertake the formalisation by translation into state-transition languages. The verification is afterwards performed by model-checking. However, one important issue raised by model checking is the state space explosion. The purpose of this paper will mainly address this issue. It is threefold. We first propose an approach to mark the derived formalisms starting from any time of the system lifecycle. The marking is drawn from the object and sequence diagrams. We secondly exploit the association ends modelled on the object diagram to retrieve the first action of each object behaviour. This contribution ensures a strong consistency when handling the object and sequence diagrams. We finally propose a method based on the association end formalisation in order to deal with the models validation. The whole of the solution is analysed by model checking.
Keywords: UML2; object diagrams; sequence diagrams; object Petri nets; model verification; model validation; UML semantics; model checking; state space explosion; modelling; object-oriented modelling; OOM.
International Journal of Computer Applications in Technology, 2013 Vol.47 No.2/3, pp.162 - 171
Published online: 05 Jun 2013 *Full-text access for editors Access for subscribers Purchase this article Comment on this article