{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T23:40:11Z","timestamp":1778542811213,"version":"3.51.4"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,5,30]],"date-time":"2018-05-30T00:00:00Z","timestamp":1527638400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Inf Syst Front"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s10796-018-9860-9","type":"journal-article","created":{"date-parts":[[2018,5,30]],"date-time":"2018-05-30T06:06:51Z","timestamp":1527660411000},"page":"45-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Verification of Model Transformations Using Isabelle\/HOL and Scala"],"prefix":"10.1007","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3754-8718","authenticated-orcid":false,"given":"Said","family":"Meghzili","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Allaoua","family":"Chaoui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Strecker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elhillali","family":"Kerkouche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,30]]},"reference":[{"key":"9860_CR1","unstructured":"Acceleo (2018): \n                    www.acceleo.org"},{"key":"9860_CR2","doi-asserted-by":"crossref","unstructured":"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\u20136","DOI":"10.1109\/INMIC.2007.4557693"},{"key":"9860_CR3","doi-asserted-by":"publisher","unstructured":"Amrani, M., Combemale, B., L\u00facio, L., Selim, G.M.K., Dingel, J., Le Traon, Y., Vangheluwe, H., Cordy, J.R.: \u201cFormal verification techniques for model transformations: A tridimensional classification\u201d. JOT 14(3), 1\u201343 (2015). \n                    https:\/\/doi.org\/10.5381\/jot.2015.14.3.a1\n                    \n                  .","DOI":"10.5381\/jot.2015.14.3.a1"},{"issue":"5","key":"9860_CR4","doi-asserted-by":"publisher","first-page":"805","DOI":"10.1007\/s00165-016-0388-9","volume":"28","author":"\u00c9 Andr\u00e9","year":"2016","unstructured":"Andr\u00e9, \u00c9., Benmoussa, M. M., & Choppy, C. (2016). Formalising concurrent UML state machines using coloured petri nets. Formal Asp Comput, 28(5), 805\u2013845. \n                    https:\/\/doi.org\/10.1007\/s00165-016-0388-9\n                    \n                  .","journal-title":"Formal Asp Comput"},{"key":"9860_CR5","doi-asserted-by":"crossref","unstructured":"Asztalos M, Lengyel L, Levendovszky T (2009) A formalism for describing modeling transformations for verification. In: MoDeVVA\u201909, Denver, Colorado","DOI":"10.1145\/1656485.1656487"},{"key":"9860_CR6","doi-asserted-by":"crossref","unstructured":"Asztalos M, Lengyel L, Levendovszky T (2010) Towards automated, formal verification of model transformations. In ICST","DOI":"10.1109\/ICST.2010.42"},{"key":"9860_CR7","unstructured":"AToM3 (2018) A Tool for Multi-formalism Meta-Modelling: \n                    atom3.cs.mcgill.ca\n                    \n                  \/"},{"key":"9860_CR8","unstructured":"AtomPM (2018): \n                    https:\/\/msdl.uantwerpen.be\/documentation\/AToMPM\/"},{"key":"9860_CR9","unstructured":"Baklanova N, Brenas JH, Echahed R, Percebois C, Strecker M, Tran HN (2015) \u201cProvably Correct Graph Transformations with Small-tALC.\u201d ICTERI"},{"key":"9860_CR10","unstructured":"Blech JO, Glesner S, Leitner J (2005) Formal verification of java code generation from UML models. In: Fujaba Days"},{"key":"9860_CR11","doi-asserted-by":"publisher","unstructured":"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\u201353. \n                    https:\/\/doi.org\/10.1016\/j.scico.2015.03.003\n                    \n                  .","DOI":"10.1016\/j.scico.2015.03.003"},{"key":"9860_CR12","unstructured":"CPN Tools Homepage (2018), \n                    http:\/\/cpntools.org\n                    \n                  \/"},{"key":"9860_CR13","doi-asserted-by":"publisher","unstructured":"da Costa Cavalheiro SA, Foss L, Ribeiro L (2017) Theorem prover graph grammars with attributes and negative application conditions. Theor Comput Sci 686: 25\u201377, ISSN 0304\u20133975, \n                    https:\/\/doi.org\/10.1016\/j.tcs.2017.04.010\n                    \n                  . (\n                    http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397517303419\n                    \n                  )","DOI":"10.1016\/j.tcs.2017.04.010"},{"key":"9860_CR14","unstructured":"De Busser J (2018), Model checking AToMPM transformation systems with Groove. Technical report, MSDL LAB, McGill University, Canada"},{"key":"9860_CR15","doi-asserted-by":"crossref","unstructured":"Djaaboub S, Kerkouche E, Chaoui A (2015) From UML Statecharts to LOTOS expressions using graph transformation. 21st international conference, ICIST, pp 548\u2013559","DOI":"10.1007\/978-3-319-24770-0_47"},{"key":"9860_CR16","doi-asserted-by":"publisher","unstructured":"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. \n                    https:\/\/doi.org\/10.1007\/s10270-017-0591-z\n                    \n                  .","DOI":"10.1007\/s10270-017-0591-z"},{"key":"9860_CR17","unstructured":"Gogolla M, Hamann L, Hilken F (2014) Checking transformation model properties with a UML and OCL model validator. VOLT@STAF : 16\u201325"},{"key":"9860_CR18","unstructured":"Haftmann F, Bulwahn L (2009) Code generation from specifications in higher-order logic. Technical University Munich , pp. 1\u2013125"},{"issue":"3","key":"9860_CR19","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D. (1987). Statecharts: A visual formalism for complex systems. Sci Comput Program, 8(3), 231\u2013274.","journal-title":"Sci Comput Program"},{"key":"9860_CR20","unstructured":"Isabelle Homepage (2018), \n                    https:\/\/isabelle.in.tum.de\/"},{"key":"9860_CR21","doi-asserted-by":"publisher","first-page":"25","DOI":"10.5381\/jot.2010.9.4.a2","volume":"9","author":"E Kerkouche","year":"2010","unstructured":"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\u201343. \n                    https:\/\/doi.org\/10.5381\/jot.2010.9.4.a2\n                    \n                  .","journal-title":"J Object Technol"},{"key":"9860_CR22","unstructured":"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\u20130764), July 2014"},{"key":"9860_CR23","doi-asserted-by":"publisher","unstructured":"Kherbouche OM, Ahmad A, Basson H (2013) Using model checking to control the structural errors in BPMN models\u201d. RCIS: 1\u201312. \n                    https:\/\/doi.org\/10.1109\/RCIS.2013.6577723\n                    \n                  .","DOI":"10.1109\/RCIS.2013.6577723"},{"key":"9860_CR24","unstructured":"Liu S (2014) Formalizing UML state machines semantics for formal analysis\u2013Asurvey. National University of Singapore lius87@comp.nus.edu.sg March 21"},{"key":"9860_CR25","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10270-014-0429-x","volume":"15","author":"L L\u00facio","year":"2016","unstructured":"L\u00facio, 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\u2013684. \n                    https:\/\/doi.org\/10.1007\/s10270-014-0429-x\n                    \n                  .","journal-title":"Softw Syst Model"},{"key":"9860_CR26","doi-asserted-by":"publisher","unstructured":"Makhlouf A, Tran HN, Percebois C, Strecker M (2016) Combining dynamic and static analysis to help develop correct graph transformations. TAP. \n                    https:\/\/doi.org\/10.1007\/978-3-319-41135-4_11","DOI":"10.1007\/978-3-319-41135-4_11"},{"key":"9860_CR27","doi-asserted-by":"publisher","unstructured":"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\u201329. \n                    https:\/\/doi.org\/10.1109\/ICAASE.2016.7843859\n                    \n                  .","DOI":"10.1109\/ICAASE.2016.7843859"},{"key":"9860_CR28","doi-asserted-by":"publisher","unstructured":"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\u2013426. \n                    https:\/\/doi.org\/10.1109\/IRI.2017.63\n                    \n                  .","DOI":"10.1109\/IRI.2017.63"},{"key":"9860_CR29","unstructured":"Meseguer J (2011) \u201cMaude\u201d. Encyclopedia of Parallel Computing Springer: 1095\u20131102"},{"key":"9860_CR30","unstructured":"Miloudi, KE, Ettouhami A (2015) A multi-view approach for formalizing UML State Machine Diagrams Using Z Notation."},{"key":"9860_CR31","doi-asserted-by":"publisher","unstructured":"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\u2013300. \n                    https:\/\/doi.org\/10.1109\/ISSRE.2012.7\n                    \n                  .","DOI":"10.1109\/ISSRE.2012.7"},{"key":"9860_CR32","doi-asserted-by":"publisher","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) \u201cIsabelle\/HOL: a proof assistant for higher-order logic\u201d, Springer-Verlag Berlin, Heidelberg \u00a92002. \n                    https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"9860_CR33","unstructured":"Object Management Group (2018): \n                    www.omg.org\/"},{"key":"9860_CR34","unstructured":"OMG. Object Modeling Group (2005) Unified modeling language specification, version 2.0, July 2005"},{"key":"9860_CR35","doi-asserted-by":"publisher","unstructured":"Percebois C, Strecker M, Tran HN (2013) Rule-level verification of graph transformations for invariants based on edges\u2019 transitive closure. In: Hierons, R.M., Merayo, M.G., Bravetti, M., (eds), Software Engineerin and formal methods, Madrid, Spain, 25\/09\/2013\u201327\/09\/2013. Volume 8137 of lecture notes in computer science, \n                    http:\/\/www.springerlink.com\n                    \n                  , Springer 106\u2013121. \n                    https:\/\/doi.org\/10.1007\/978-3-642-40561-7_8\n                    \n                  .","DOI":"10.1007\/978-3-642-40561-7_8"},{"key":"9860_CR36","doi-asserted-by":"publisher","unstructured":"Poizat P, Sala\u00fcn G, Krishna A (2016) Checking Business Process Evolution. FACS. \n                    https:\/\/doi.org\/10.1007\/978-3-319-57666-4_4","DOI":"10.1007\/978-3-319-57666-4_4"},{"key":"9860_CR37","unstructured":"PVS Specification and Verification System (2018): \n                    https:\/\/pvs.csl.sri.com\/"},{"key":"9860_CR38","doi-asserted-by":"publisher","unstructured":"Rensink A (2003) The GROOVE simulator: A tool for state space generation. AGTIVE : 479\u2013485. \n                    https:\/\/doi.org\/10.1007\/978-3-540-25959-6_40\n                    \n                  .","DOI":"10.1007\/978-3-540-25959-6_40"},{"key":"9860_CR39","doi-asserted-by":"publisher","unstructured":"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\u20131. \n                    https:\/\/doi.org\/10.1109\/TSE.2016.2635137\n                    \n                  .","DOI":"10.1109\/TSE.2016.2635137"},{"key":"9860_CR40","doi-asserted-by":"publisher","unstructured":"Sch\u00e4tz B (2010) Verification of model transformations. ECEASST 29. \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.29.420","DOI":"10.14279\/tuj.eceasst.29.420"},{"key":"9860_CR41","unstructured":"StarUML, staruml.io\/ (2018)"},{"key":"9860_CR42","doi-asserted-by":"publisher","unstructured":"Strecker M (2002) Formal verification of a Java Compiler in Isabelle. International Conference on Automated Deduction (CADE), Berlin, Heidelberg, pp. 63-77. \n                    https:\/\/doi.org\/10.1007\/3-540-45620-1_5\n                    \n                  .","DOI":"10.1007\/3-540-45620-1_5"},{"key":"9860_CR43","unstructured":"TGG (2018):\n                    http:\/\/www-old.cs.uni-paderborn.de\/en\/research-group\/software-engineering\/research\/projects\/tgg-interpreter.html"},{"key":"9860_CR44","unstructured":"The <AGG> Homepage (2018): \n                    http:\/\/www.user.tu-berlin.de\/o.runge\/agg\/"},{"key":"9860_CR45","unstructured":"The Coq Proof Assistant (2018): \n                    https:\/\/coq.inria.fr\/"},{"key":"9860_CR46","unstructured":"The Standard ML Programming Language (2018): \n                    http:\/\/www.macs.hw.ac.uk\/ultra\/skalpel\/html\/sml.html"},{"key":"9860_CR47","unstructured":"Topology and Orchestration Specification for Cloud Applications Version 1.0. 25 November (2013). OASIS Standard. \n                    http:\/\/docs.oasis-open.org\/tosca\/TOSCA\/v1.0\/os\/TOSCA-v1.0-os.html\n                    \n                  ."},{"key":"9860_CR48","doi-asserted-by":"publisher","unstructured":"Van der Aalst WM, Stahl C, Westergaard M (2013) Strategies for modeling complex processes using colored petri nets.\u201dIn: Transactions on petri nets and other models of concurrency vii (pp. 6\u201355). Springer Berlin Heidelberg. \n                    https:\/\/doi.org\/10.1007\/978-3-642-38143-0_2","DOI":"10.1007\/978-3-642-38143-0_2"},{"key":"9860_CR49","unstructured":"Varr\u00f3 D, Pataricza A (2003) Automated formal verification of model transformations. In: CSDUML, pp. 63\u201378"},{"key":"9860_CR50","doi-asserted-by":"publisher","unstructured":"Wei X, Dong Y, Li X, Wong WE (2017) Architecture-level hazard analysis using AADL. J Syst Softw, ISSN 0164-1212, \n                    https:\/\/doi.org\/10.1016\/j.jss.2017.06.018\n                    \n                  .","DOI":"10.1016\/j.jss.2017.06.018"},{"key":"9860_CR51","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.entcs.2012.06.009","volume":"285","author":"M Wenzel","year":"2012","unstructured":"Wenzel, M. (2012). Asynchronous proof processing with Isabelle\/Scala and Isabelle\/jEdit. Electr Notes Theor Comput Sci, 285, 101\u2013114. \n                    https:\/\/doi.org\/10.1016\/j.entcs.2012.06.009\n                    \n                  .","journal-title":"Electr Notes Theor Comput Sci"},{"key":"9860_CR52","unstructured":"Zhang SJ, Liu Y (2010) \u201cAn Automatic Approach to Model Checking UML State Machines.\u201d 2010 Fourth international conference on secure software integration and reliability improvement companion, Singapore, pp. 1\u20136"}],"container-title":["Information Systems Frontiers"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10796-018-9860-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10796-018-9860-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10796-018-9860-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T19:18:33Z","timestamp":1559157513000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10796-018-9860-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,30]]},"references-count":52,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["9860"],"URL":"https:\/\/doi.org\/10.1007\/s10796-018-9860-9","relation":{},"ISSN":["1387-3326","1572-9419"],"issn-type":[{"value":"1387-3326","type":"print"},{"value":"1572-9419","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,30]]},"assertion":[{"value":"30 May 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}