Advertisement

Information Systems Frontiers

, Volume 21, Issue 1, pp 45–65 | Cite as

Verification of Model Transformations Using Isabelle/HOL and Scala

  • Said MeghziliEmail author
  • Allaoua Chaoui
  • Martin Strecker
  • Elhillali Kerkouche
Article

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 

References

  1. Acceleo (2018): www.acceleo.org
  2. 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–6Google Scholar
  3. 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.
  4. 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.CrossRefGoogle Scholar
  5. Asztalos M, Lengyel L, Levendovszky T (2009) A formalism for describing modeling transformations for verification. In: MoDeVVA’09, Denver, ColoradoGoogle Scholar
  6. Asztalos M, Lengyel L, Levendovszky T (2010) Towards automated, formal verification of model transformations. In ICSTGoogle Scholar
  7. AToM3 (2018) A Tool for Multi-formalism Meta-Modelling: atom3.cs.mcgill.ca/
  8. Baklanova N, Brenas JH, Echahed R, Percebois C, Strecker M, Tran HN (2015) “Provably Correct Graph Transformations with Small-tALC.” ICTERIGoogle Scholar
  9. Blech JO, Glesner S, Leitner J (2005) Formal verification of java code generation from UML models. In: Fujaba DaysGoogle Scholar
  10. 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.
  11. CPN Tools Homepage (2018), http://cpntools.org/
  12. 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)
  13. De Busser J (2018), Model checking AToMPM transformation systems with Groove. Technical report, MSDL LAB, McGill University, CanadaGoogle Scholar
  14. Djaaboub S, Kerkouche E, Chaoui A (2015) From UML Statecharts to LOTOS expressions using graph transformation. 21st international conference, ICIST, pp 548–559Google Scholar
  15. 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.
  16. Gogolla M, Hamann L, Hilken F (2014) Checking transformation model properties with a UML and OCL model validator. VOLT@STAF : 16–25Google Scholar
  17. Haftmann F, Bulwahn L (2009) Code generation from specifications in higher-order logic. Technical University Munich , pp. 1–125Google Scholar
  18. Harel, D. (1987). Statecharts: A visual formalism for complex systems. Sci Comput Program, 8(3), 231–274.CrossRefGoogle Scholar
  19. Isabelle Homepage (2018), https://isabelle.in.tum.de/
  20. 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.CrossRefGoogle Scholar
  21. 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 2014Google Scholar
  22. 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.
  23. Liu S (2014) Formalizing UML state machines semantics for formal analysis–Asurvey. National University of Singapore lius87@comp.nus.edu.sg March 21Google Scholar
  24. 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.CrossRefGoogle Scholar
  25. 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
  26. 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.
  27. 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.
  28. Meseguer J (2011) “Maude”. Encyclopedia of Parallel Computing Springer: 1095–1102Google Scholar
  29. Miloudi, KE, Ettouhami A (2015) A multi-view approach for formalizing UML State Machine Diagrams Using Z Notation.Google Scholar
  30. 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.
  31. Nipkow T, Paulson LC, Wenzel M (2002) “Isabelle/HOL: a proof assistant for higher-order logic”, Springer-Verlag Berlin, Heidelberg ©2002.  https://doi.org/10.1007/3-540-45949-9
  32. Object Management Group (2018): www.omg.org/
  33. OMG. Object Modeling Group (2005) Unified modeling language specification, version 2.0, July 2005Google Scholar
  34. 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.
  35. Poizat P, Salaün G, Krishna A (2016) Checking Business Process Evolution. FACS.  https://doi.org/10.1007/978-3-319-57666-4_4
  36. PVS Specification and Verification System (2018): https://pvs.csl.sri.com/
  37. 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.
  38. 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.
  39. Schätz B (2010) Verification of model transformations. ECEASST 29.  https://doi.org/10.14279/tuj.eceasst.29.420
  40. StarUML, staruml.io/ (2018)Google Scholar
  41. 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.
  42. The <AGG> Homepage (2018): http://www.user.tu-berlin.de/o.runge/agg/
  43. The Coq Proof Assistant (2018): https://coq.inria.fr/
  44. The Standard ML Programming Language (2018): http://www.macs.hw.ac.uk/ultra/skalpel/html/sml.html
  45. 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.
  46. 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
  47. Varró D, Pataricza A (2003) Automated formal verification of model transformations. In: CSDUML, pp. 63–78Google Scholar
  48. 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.
  49. 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.CrossRefGoogle Scholar
  50. 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–6Google Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2018

Authors and Affiliations

  1. 1.MISC Laboratory, Computer Science DepartmentUniversity of ConstantineConstantineAlgeria
  2. 2.IRITUniversity of Paul SabatierToulouseFrance
  3. 3.Computer Science DepartmentUniversity of JijelJijelAlgeria

Personalised recommendations