A Property-Driven Approach to Formal Verification of Process Models

Benoit Combemale (1) , Xavier Crégut (1, 2) , Pierre-Loïc Garoche (3) , Xavier Thirioux (3) , François Vernadat (4)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 Toulouse INP - Institut National Polytechnique (Toulouse)
3 IRIT - Institut de recherche en informatique de Toulouse
4 LAAS - Laboratoire d'analyse et d'architecture des systèmes

More and more, models, through Domain Specific Languages (DSL), tend to be the solution to define complex systems. Expressing properties specific to these metamodels, and checking them, appear as an urgent need. Until now, the only complete industrial solutions that are available consider structural properties such as the ones that could be expressed in OCL. There are although some attempts on behavioural properties for DSL. This paper addresses a method to specify and then check temporal properties over models. The case study is SimplePDL, a process metamodel. We propose a way to use a temporal extension of OCL, TOCL, to express properties. We specify a models transformation to Petri Nets and LTL formulae for both the process model and its associated temporal properties. We check these properties using a model checker and enrich the model with the analysis results. This work is a first step towards a generic framework to specify and effectively check temporal properties over arbitrary models.

Mots clés: Verification; Temporal OCL; Models Semantics; Process Model; LTL; Model Transformation; Petri Nets; Properties Validation; Metamodelling

Domaines: Génie logiciel [cs.SE]

Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux, François Vernadat. A Property-Driven Approach to Formal Verification of Process Models. Enterprise Information Systems, 2008, 12, pp.286-300. ⟨10.1007/978-3-540-88710-2⟩. ⟨hal-00369884⟩