Verification of Model Transformations Using Isabelle/HOL and Scala

Said Meghzili (), Allaoua Chaoui (), Martin Strecker and Elhillali Kerkouche
Additional contact information
Said Meghzili: University of Constantine
Allaoua Chaoui: University of Constantine
Martin Strecker: University of Paul Sabatier
Elhillali Kerkouche: University of Constantine

Information Systems Frontiers, 2019, vol. 21, issue 1, No 4, 45-65

Abstract: Abstract Model transformations have proved to be powerful in the development of critical systems. According to their intents, they have been used in many domains such as models refinement, simulation, and domain semantics. The formal methods have been successful in the verification and validation of critical systems, and in particular, in the formalization of UML, BPMN, and AADL. However, little research has been done on verifying the transformation itself. In this paper, we extend our previous work using Isabelle/HOL that transforms UML State Machine Diagrams (SMD) to Colored Petri nets (CPN) models and proves that certain structural properties of this transformation are correct. For example, the structural property: “for each final state of a SMD model a corresponding place in CPN model should be generated by the transformation” is described and checked using Isabelle/HOL as invariant property. In the current work, we use Scala as environment of executing Isabelle/HOL specifications and we perform the verified transformation using Scala. Moreover, we demonstrate our approach using another case study of transforming BPMN (Business Process Model and Notation) models into Petri nets models and verify the correctness of certain structural properties of this transformation.

Keywords: Model-driven engineering (MDE); UML; Colored petri nets (CPN); Business process; Model transformation; Transformation correctness; Formal verification; Theorem Prover (search for similar items in EconPapers)
Date: 2019
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
http://link.springer.com/10.1007/s10796-018-9860-9 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:infosf:v:21:y:2019:i:1:d:10.1007_s10796-018-9860-9

Ordering information: This journal article can be ordered from
http://www.springer.com/journal/10796

DOI: 10.1007/s10796-018-9860-9

Access Statistics for this article

Information Systems Frontiers is currently edited by Ram Ramesh and Raghav Rao

More articles in Information Systems Frontiers from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().