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.
Mots clés :
Model-driven engineering (MDE)
UML
Colored petri nets (CPN)
Business process
Model transformation
Transformation correctness
Formal verification
Theorem Prover
S. Meghzili, A. Chaoui, M. Strecker and E. Kerkouche. 2018. Verification of Model Transformations Using Isabelle/HOL and Scala. Information Systems Frontiers (May 2018), Springer. DOI: https://doi.org/10.1007/s10796-018-9860-9.
APA :
Meghzili, S., Chaoui, A., Strecker, M. & Kerkouche, E. (2018, May). Verification of Model Transformations Using Isabelle/HOL and Scala. Information Systems Frontiers, Springer. DOI: https://doi.org/10.1007/s10796-018-9860-9
IEEE :
S. Meghzili, A. Chaoui, M. Strecker and E. Kerkouche, "Verification of Model Transformations Using Isabelle/HOL and Scala". Information Systems Frontiers, Springer, May, 2018. DOI: https://doi.org/10.1007/s10796-018-9860-9.
BibTeX :
@article{misc-lab-170, author = {Meghzili, Said and Chaoui, Allaoua and Strecker, Martin and Kerkouche, Elhillali}, title = {Verification of Model Transformations Using Isabelle/HOL and Scala}, journal = {Information Systems Frontiers}, issn = {1572-9419}, publisher = {Springer}, year = {2018}, month = {May}, doi = {10.1007/s10796-018-9860-9}, url = {https://link.springer.com/article/10.1007%2Fs10796-018-9860-9}, keywords = {Model-driven engineering (MDE), UML, Colored petri nets (CPN), Business process, Model transformation, Transformation correctness, Formal verification, Theorem Prover} }
RIS :
TI - Verification of Model Transformations Using Isabelle/HOL and Scala AU - S. Meghzili AU - A. Chaoui AU - M. Strecker AU - E. Kerkouche PY - 2018 SN - 1572-9419 JO - Information Systems Frontiers PB - Springer AB - 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. KW - Model-driven engineering (MDE) KW - UML KW - Colored petri nets (CPN) KW - Business process KW - Model transformation KW - Transformation correctness KW - Formal verification KW - Theorem Prover DO - 10.1007/s10796-018-9860-9 UR - https://link.springer.com/article/10.1007%2Fs10796-018-9860-9 ID - misc-lab-170 ER -