nach oben

Information Systems Frontiers

Erschienen in:

30.05.2018

Verification of Model Transformations Using Isabelle/HOL and Scala

verfasst von: Said Meghzili, Allaoua Chaoui, Martin Strecker, Elhillali Kerkouche

Erschienen in: Information Systems Frontiers | Ausgabe 1/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Towards a Reuse Strategic Decision Pattern Framework – from Theories to Practices

Nächster Artikel Quantitative Analysis of Apache Storm Applications: The NewsAsset Case Study

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Acceleo (2018): www.acceleo.org

Ali T, Nauman M, Alam M (2007) An Accessible Formal Specification of the UML and OCL Meta-Model in Isabelle/HOL. 2007 IEEE international multitopic conference, Lahore, pp. 1–6

Amrani, M., Combemale, B., Lúcio, L., Selim, G.M.K., Dingel, J., Le Traon, Y., Vangheluwe, H., Cordy, J.R.: “Formal verification techniques for model transformations: A tridimensional classification”. JOT 14(3), 1–43 (2015). https://doi.org/10.5381/jot.2015.14.3.a1.

André, É., Benmoussa, M. M., & Choppy, C. (2016). Formalising concurrent UML state machines using coloured petri nets. Formal Asp Comput, 28(5), 805–845. https://doi.org/10.1007/s00165-016-0388-9.CrossRef

Asztalos M, Lengyel L, Levendovszky T (2009) A formalism for describing modeling transformations for verification. In: MoDeVVA’09, Denver, Colorado

Asztalos M, Lengyel L, Levendovszky T (2010) Towards automated, formal verification of model transformations. In ICST

AToM³ (2018) A Tool for Multi-formalism Meta-Modelling: atom3.cs.mcgill.ca/

AtomPM (2018): https://msdl.uantwerpen.be/documentation/AToMPM/

Baklanova N, Brenas JH, Echahed R, Percebois C, Strecker M, Tran HN (2015) “Provably Correct Graph Transformations with Small-tALC.” ICTERI

Blech JO, Glesner S, Leitner J (2005) Formal verification of java code generation from UML models. In: Fujaba Days

Bodeveix J-P, Filali M, Garnacho M, Spadotti R, Yang Z (2015) Towards a verified transformation from AADL to the formal component-based language FIACRE. In: Science of Computer Programming, Elsevier, vol. 106, pp. 30–53. https://doi.org/10.1016/j.scico.2015.03.003.

CPN Tools Homepage (2018), http://cpntools.org/

da Costa Cavalheiro SA, Foss L, Ribeiro L (2017) Theorem prover graph grammars with attributes and negative application conditions. Theor Comput Sci 686: 25–77, ISSN 0304–3975, https://doi.org/10.1016/j.tcs.2017.04.010. (http://www.sciencedirect.com/science/article/pii/S0304397517303419)

De Busser J (2018), Model checking AToMPM transformation systems with Groove. Technical report, MSDL LAB, McGill University, Canada

Djaaboub S, Kerkouche E, Chaoui A (2015) From UML Statecharts to LOTOS expressions using graph transformation. 21st international conference, ICIST, pp 548–559

Gabmeyer, S., Kaufmann, P., Seidl, M., Gogolla, M., & Kappel, G. (2017). A feature-based classification of formal verification techniques for software models. Softw Syst Model. https://doi.org/10.1007/s10270-017-0591-z.

Gogolla M, Hamann L, Hilken F (2014) Checking transformation model properties with a UML and OCL model validator. VOLT@STAF : 16–25

Haftmann F, Bulwahn L (2009) Code generation from specifications in higher-order logic. Technical University Munich , pp. 1–125

Harel, D. (1987). Statecharts: A visual formalism for complex systems. Sci Comput Program, 8(3), 231–274.CrossRef

Isabelle Homepage (2018), https://isabelle.in.tum.de/

Kerkouche, E., Chaoui, A., Bourennane, E.-B., & Labbani, O. (2010). A UML and colored petri nets integrated modeling and analysis approach using graph transformation. J Object Technol, 9, 25–43. https://doi.org/10.5381/jot.2010.9.4.a2.CrossRef

Kerkouche E, Elmansouri R, Chaoui A, Khalfaoui K (2014) An automatic approach to Verify business process models using INA petri nets analyzer. Int J Comput Inf Technol 3(4)(ISSN: 2279–0764), July 2014

Kherbouche OM, Ahmad A, Basson H (2013) Using model checking to control the structural errors in BPMN models”. RCIS: 1–12. https://doi.org/10.1109/RCIS.2013.6577723.

Liu S (2014) Formalizing UML state machines semantics for formal analysis–Asurvey. National University of Singapore lius87@comp.nus.edu.sg March 21

Lúcio, L., Amrani, M., Dingel, J., Lambers, L., Salay, R., Selim, G. M. K., Syriani, E., & Wimmer, M. (2016). Model transformation intents and their properties. Softw Syst Model, 15, 647–684. https://doi.org/10.1007/s10270-014-0429-x.CrossRef

Makhlouf A, Tran HN, Percebois C, Strecker M (2016) Combining dynamic and static analysis to help develop correct graph transformations. TAP. https://doi.org/10.1007/978-3-319-41135-4_11

Meghzili S, Chaoui A, Strecker M, Kerkouche E (2016) Transformation and validation of BPMN models to petri nets models using GROOVE," 2016 International Conference on Advanced Aspects of Software Engineering (ICAASE), Constantine, pp. 22–29. https://doi.org/10.1109/ICAASE.2016.7843859.

Meghzili AC, Strecker M, Kerkouche E (2017) On the verification of UML state machine diagrams to colored petri nets transformation using Isabelle/HOL. IEEE International Conference on Information Reuse and Integration (IRI), San Diego, CA, 2017, pp. 419–426. https://doi.org/10.1109/IRI.2017.63.

Meseguer J (2011) “Maude”. Encyclopedia of Parallel Computing Springer: 1095–1102

Miloudi, KE, Ettouhami A (2015) A multi-view approach for formalizing UML State Machine Diagrams Using Z Notation.

Mottu JM, Sen S, Tisi M, Cabot J (2012) static analysis of model transformations for effective test generation. 2012 IEEE 23rd international symposium on software reliability engineering, Dallas, TX, pp. 291–300. https://doi.org/10.1109/ISSRE.2012.7.

Object Management Group (2018): www.omg.org/

OMG. Object Modeling Group (2005) Unified modeling language specification, version 2.0, July 2005

Percebois C, Strecker M, Tran HN (2013) Rule-level verification of graph transformations for invariants based on edges’ transitive closure. In: Hierons, R.M., Merayo, M.G., Bravetti, M., (eds), Software Engineerin and formal methods, Madrid, Spain, 25/09/2013–27/09/2013. Volume 8137 of lecture notes in computer science, http://www.springerlink.com, Springer 106–121. https://doi.org/10.1007/978-3-642-40561-7_8.

Poizat P, Salaün G, Krishna A (2016) Checking Business Process Evolution. FACS. https://doi.org/10.1007/978-3-319-57666-4_4

PVS Specification and Verification System (2018): https://pvs.csl.sri.com/

Rensink A (2003) The GROOVE simulator: A tool for state space generation. AGTIVE : 479–485. https://doi.org/10.1007/978-3-540-25959-6_40.

Sanchez Cuadrado J; Guerra E; J. de Lara (2016) Static analysis of model transformations. In: IEEE transactions on software engineering, vol. PP, no. 99, pp. 1–1. https://doi.org/10.1109/TSE.2016.2635137.

Schätz B (2010) Verification of model transformations. ECEASST 29. https://doi.org/10.14279/tuj.eceasst.29.420

StarUML, staruml.io/ (2018)

Strecker M (2002) Formal verification of a Java Compiler in Isabelle. International Conference on Automated Deduction (CADE), Berlin, Heidelberg, pp. 63-77. https://doi.org/10.1007/3-540-45620-1_5.

TGG (2018):http://www-old.cs.uni-paderborn.de/en/research-group/software-engineering/research/projects/tgg-interpreter.html

The <AGG> Homepage (2018): http://www.user.tu-berlin.de/o.runge/agg/

The Coq Proof Assistant (2018): https://coq.inria.fr/

The Standard ML Programming Language (2018): http://www.macs.hw.ac.uk/ultra/skalpel/html/sml.html

Topology and Orchestration Specification for Cloud Applications Version 1.0. 25 November (2013). OASIS Standard. http://docs.oasis-open.org/tosca/TOSCA/v1.0/os/TOSCA-v1.0-os.html.

Van der Aalst WM, Stahl C, Westergaard M (2013) Strategies for modeling complex processes using colored petri nets.”In: Transactions on petri nets and other models of concurrency vii (pp. 6–55). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-38143-0_2

Varró D, Pataricza A (2003) Automated formal verification of model transformations. In: CSDUML, pp. 63–78

Wei X, Dong Y, Li X, Wong WE (2017) Architecture-level hazard analysis using AADL. J Syst Softw, ISSN 0164-1212, https://doi.org/10.1016/j.jss.2017.06.018.

Wenzel, M. (2012). Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit. Electr Notes Theor Comput Sci, 285, 101–114. https://doi.org/10.1016/j.entcs.2012.06.009.CrossRef

Zhang SJ, Liu Y (2010) “An Automatic Approach to Model Checking UML State Machines.” 2010 Fourth international conference on secure software integration and reliability improvement companion, Singapore, pp. 1–6

Titel: Verification of Model Transformations Using Isabelle/HOL and Scala
verfasst von: Said Meghzili
Allaoua Chaoui
Martin Strecker
Elhillali Kerkouche
Publikationsdatum: 30.05.2018
Verlag: Springer US
Erschienen in: Information Systems Frontiers / Ausgabe 1/2019
Print ISSN: 1387-3326
Elektronische ISSN: 1572-9419
DOI: https://doi.org/10.1007/s10796-018-9860-9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 1/2019

Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics

Generalized Feature Embedding for Supervised, Unsupervised, and Online Learning Tasks

Exploiting Repositories in Mobile Software Ecosystems from a Governance Perspective

Extracting Knowledge from Technical Reports for the Valuation of West Texas Intermediate Crude Oil Futures

An examination of the long-term business value of investments in information technology

Discovering composable web services using functional semantics and service dependencies based on natural language requests