Authors: Miloud Bennama; Thouraya Bouabana-Tebibel
Addresses: Laboratoire de Communication dans les Systèmes Informatiques (LCSI), Ecole Nationale Supérieure d'Informatique (ESI), BP 68M Oued-Smar 16309 Alger, Algeria ' Laboratoire de Communication dans les Systèmes Informatiques (LCSI), Ecole Nationale Supérieure d'Informatique (ESI), BP 68M Oued-Smar 16309 Alger, Algeria
Abstract: OCL has been integrated to UML as a modern and formal modelling language, which is easy to learn and efficient to use. UML is a semi-formal language that does not support validation tasks. Petri nets serve as a formalism defining a denotational semantics for the notation. The derived Petri nets are validated using system properties. These properties are written in temporal logic to be validated on the derived Petri nets. The purpose of this paper is to assist the UML modeller, not necessarily familiar with Petri nets and temporal logics, in the validation process. Thus, our contribution is two-fold. We propose to extend OCL invariants and pre/post-conditions with temporal operators. The user expresses system properties in OCL. Next, we transform the extended OCL constraints to CTL-Like temporal logic based on SML language for verification in the CPNtools model-checker. The analysis results are in the form of CPNtools reports, incomprehensible to the user. We interpret and return them to the user in UML language.
Keywords: UML validation; interaction overview diagram; IOD; Object Constraint Language; OCL; standard ML; SML; temporal logic extension; Petri nets; CPNtools; mapping; model checking.
International Journal of Critical Computer-Based Systems, 2016 Vol.6 No.4, pp.302 - 321
Published online: 25 Jan 2017 *Full-text access for editors Access for subscribers Purchase this article Comment on this article