Title: A CTL-based OCL extension using CPN ML for UML validation

 

Author: 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

 

Journal: Int. J. of Critical Computer-Based Systems, 2016 Vol.6, No.4, pp.302 - 321

 

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.

 

DOI: http://dx.doi.org/10.1504/IJCCBS.2016.081807

 

Available online 25 Jan 2017

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article