Abstract
In Model Driven Software Engineering, models and model transformations are the primary artifacts when developing a software system. In such a workflow, model transformations are used to incrementally transform initial abstract models into concrete models containing all relevant system details. Over the years, various formal methods have been proposed and further developed to determine the functional correctness of models of concurrent systems. However, the formal verification of model transformations has so far not received as much attention. In this article, we propose a formal verification technique to determine that formalisations of such transformations in the form of rule systems are guaranteed to preserve functional properties, regardless of the models they are applied on. This work extends our earlier work in various ways. Compared to our earlier approaches, the current technique involves only up to n individual checks, with n the number of rules in the rule system, whereas previously, up to 2n − 1 checks were required. Furthermore, a full correctness proof for the technique is presented, based on a formal proof conducted with the Coq proof assistant. Finally, we report on two sets of conducted experiments. In the first set, we compared traditional model checking with transformation verification, and in the second set, we compared the verification technique presented in this article with the previous version.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. Softw Tools Technol Transf 12(6): 447–466
Amrani M, Combemale B, Lúcio L, Selim GMK, Dingel J, Le Traon Y, Vangheluwe H, Cordy JR (2015) Formal verification techniques for model transformations: a tridimensional classification. J Object Technol 14(3): 1–43
Abadi M, Lamport L (1991) The existence of refinement mappings. Theor Comput Sci 82: 253–284
Baldan P, Corradini A, Ehrig H, Heckel R, König B (2007) Bisimilarity and behaviour-preserving reconfigurations of open petri nets. In: Proceeding of 2nd conference on algebra and coalgebra in computer science (CALCO 2007), volume 4624 of LNCS. Springer, pp 126–142
Braunstein C, Encrenaz E (2004) CTL-property transformation along an incremental design process. In: Proceeding of 4th international workshop on automated verification of critical systems, volume 128 of ENTCS. Elsevier, pp 263–278
Bal H, Epema D, de Laat C, van Nieuwpoort R, Romein J, Seinstra F, Snoek C, Wijshoff H (216) A medium-scale distributed system for computer science research: infrastructure for the long term. IEEE Comput 49(5): 54–63
Bošnački D, Edelkamp S, Sulewski D, Wijs AJ (2010) GPU-PRISM: an extension of PRISM for general purpose graphics processing units. In: Proceeding of 9th international workshop on parallel and distributed methods in verification (PDMC 2010). IEEE Computer Society Press, pp 17–19
Blech JO, Glesner S, Leitner J (2005) Formal verification of java code generation from UML models. In: 3rd international fujaba days. Fujaba Days, pp 49–56
Bowen JP, Hinchey MG (2004) Formal methods. In: Computldbook, chapter 106. ACM, pp 106–1–106–25
Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge
Combemale B, Crégut X, Garoche P-L, Thirioux X (2009) Essay on semantics definition in MDE: an instrumented approach for model verification. J Softw 4(9): 943–958
Cranen S, Groote JF, Keiren JJA, Stappers FPM, de Vink EP, Wesselink W, Willemse T (2013) An overview of the mCRL2 toolset and its recent advances. In: Proceeding of 19th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2013), volume 7795 of LNCS. Springer, pp 199–213
Dodds M, Plump D (2006) Graph transformation in constant time. In: Proceeding of 3rd international conference on graph transformation (ICGT 2006), volume 4178 of LNCS. Springer, pp 367–382
Eppstein D, Galil Z, Italiano G (1997) Dynamic graph algorithms. In: CRC handbook of algorithms and theory of computation chapter 22. CRC Press, Boca Raton
Fokkink WJ, Pang J, Wijs AJ (2005) Is timed branching bisimilarity an equivalence indeed? In: Proceeding of 3rd conference on formal modelling and analysis of timed systems (FORMATS 2005), volume 3829 of Lecture Notes in Computer Science. Springer, pp 258–272
Giese H, Glesner S, Leitner J, Schäfer W, Wagner R (2006) Towards verified model transformations. In: Proceeding of 3rd workshop on model-driven engineering, verification, and validation (MoDeVVa 2006), pp 78–93
Giese H, Lambers L (2012) Towards automatic verification of behavior preservation for model transformation via invariant checking. In: Proceeding of 6th international conference on graph transformation (ICGT 2012), volume 7562 of LNCS. Springer, pp 249–263
Garavel H, Lang F, Mateescu R, Serwe W (2011) CADP 2010: A toolbox for the construction and analysis of distributed processes. In: Proceeding of 17th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2011), volume 6605 of LNCS. Springer, pp 372–387
Garavel H, Sighireanu M (1999) A graphical parallel composition operator for process algebras. In: Proceeding of 1999 IFIP TC6/WG6.1 joint international conference on formal description techniques and protocol specification, testing and verification (FORTE/PSTV 1999), volume 156 of IFIP conference proceedings. Kluwer, pp 185–202
Groote JF, Wijs AJ (2016) An \({O(m \log n)}\) algorithm for stuttering equivalence and branching bisimulation. In: Proceeding of 22nd international conference on tools and algorithms for the construction and analysis of systems (TACAS 2016), volume 9636 of LNCS. Springer, pp 607–624
Hülsbusch M, König B, Rensink A,Semenyak M, Soltenborn C, Wehrheim H (2010) Showing full semantics preservation in model transformations: a comparison of techniques. In: Proceeding of 8th international conference on integrated formal methods (iFM 2010), volume 6396 of LNCS, pp 183–198. Springer.
Kundu S, Lerner S, Gupta R (2007) Automated refinement checking of concurrent systems. In: Proceeding of 26th international conference on computer-aided design (ICCAD 2007). IEEE, pp 318–325
Karsai G, Narayanan A (2007) On the correctness of model transformations in the development of embedded systems. In: Proceeding of 13th monterey workshop 2006, volume 4888 of LNCS. Springer, pp 1–18
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Proceeding of 23rd international conference on computer aided verification (CAV 2011), volume 6806 of LNCS. Springer, pp 585–591
Kahsai T, Roggenbach M (2008) Property preserving refinement for Csp-Casl. In: Proceeding of 19th international workshop on algebraic development techniques (WADT 2008), volume 5486 of LNCS. Springer, pp 206–220
Kleppe A, Warmer J, Bast W (2005) MDA Explained: The Model Driven Architecture(TM): Practice and Promise. Addison-Wesley Professional
Lano K (1996) The B language and method, a guide to practical formal development. Springer, New York
Lang F (2006) Refined interfaces for compositional verification. In: Proceeding of 26th international conference on formal methods for networked and distributed systems (FORTE 2006), volume 4229 of LNCS. Springer, pp 159–174
Lang F, Mateescu R (2013) Partial model checking using networks of labelled transition systems and boolean equation systems. Log Methods Comput Sci 9(4): 1–32
Luttik SP (1997) Description and formal specification of the link layer of P1394. Technical Report SEN-R9706, CWI
Mateescu R, Wijs AJ (2014) Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci Comput Program 96(3): 354–376
National Institute of Standards and Technology (1999) Data encryption standard (DES). Federal information processing standards pp 46–3
Narayanan A, Karsai G (2008) Towards verifying model transformations. In: Proceeding of 7th international workshop on graph transformation and visual modeling techniques (GT-VMT 2008), volume 211 of ENTCS. Elsevier, pp 191–200
Ploeger B (2009) Analysis of ACS using mCRL2. Technical Report 09-11, Eindhoven University of Technology
de Putter S, Wijs AJ (2016) Verifying a verifier: on the formal correctness of an LTS transformation verification technique. In: Proceeding of 19th international conference on fundamental approaches to software engineering (FASE 2016), volume 9633 of LNCS. Springer, pp 383–400
Romijn J (1999) Model checking a HAVi leader election protocol. Technical Report SEN-R9915, CWI
Ramalingam G, Reps T (1996) On the computational complexity of dynamic graph problems. Theor Comput Sci 158: 233–277
Rahim LA, Whittle J (2013) A survey of approaches for verifying model transformations. Softw Syst Model pp 1–26.
Saha D (2007) An incremental bisimulation algorithm. In: Proceeding of 27th iarcs annual conference on foundations of software technology and theoretical computer science (FSTTCS 2007), volume 4855 of LNCS. Springer, pp 204–215
Selim GMK, Lúcio L, Cordy JR, Dingel J, Oakes BJ (2014) Specification and verification of graph-based model transformation properties. In: Proceeding of 9th international colloquium on graph theory and combinatorics (ICGT 2014), volume 8571 of LNCS. Springer, pp 113–129
Stenzel K, Moebius N, Reif W (2011) Formal verification of QVT transformations for code generation. In: Proceeding of 14th international conference on model driven engineering languages and systems (MODELS 2011), volume 6981 of LNCS. Springer, pp 533–547
Sokolsky OV, Smolka SA (1994) Incremental model checking in the modal Mu-Calculus. In: Proceeding of 6th international conference on computer aided verification (CAV 1994), volume 818 of LNCS. Springer, pp 351–363
Swamy GM (1996) Incremental methods for formal verification and logic synthesis. PhD thesis, University of California
van Glabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3): 555–600
Varró D, Pataricza A (2003) Automated formal verification of model transformations. In: Proceeding of 2nd international workshop on critical systems development with UML (CSDUML 2003), pp 63–78
Wijs AJ, Engelen LJP (2013) Efficient property preservation checking of model refinements. In: Proceeding of 19th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2013), volume 7795 of LNCS. Springer, pp 565–579
Wijs AJ, Engelen LJP (2014) Refiner: towards formal verification of model transformations. In: Proceeding of 6th NASA formal methods symposium (NFM 2014), volume 8430 of LNCS. Springer, pp 258–263
Wijs AJ, Fokkink WJ (2005) From \({\chi_{\textnormal{t}}}\) to \({\mu}\) CRL: combining performance and functional analysis. In: Proceeding of 10th conference on engineering of complex computer systems (ICECCS 2005). IEEE Computer Society Press, pp 184–193
Wijs AJ (2007) Achieving discrete relative timing with untimed process algebra. In: Proceeding of 12th conference on engineering of complex computer systems (ICECCS 2007). IEEE Computer Society Press, pp 35–44
Wijs AJ (2013) Define, verify, refine: correct composition and transformation of concurrent system semantics. In: Proceeding of 10th international symposium on formal aspects of component software (FACS 2013), volume 8348 of LNCS. Springer, pp 348–368
Wijs AJ (2015) Confluence detection for transformations of labelled transition systems. In: Proceeding of 2nd graphs as models workshop (GaM 2015), volume 181 of EPTCS. Open Publishing Association, pp 1–15
Winskel G (1990) A compositional proof system on a category of labelled transition systems. Inf Comput 87(1-2): 2–57
Author information
Authors and Affiliations
Corresponding authors
Additional information
Perdita Stevens, Andrzej Wasowski, and Ewen Denney
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
de Putter, S., Wijs, A. A formal verification technique for behavioural model-to-model transformations. Form Asp Comp 30, 3–43 (2018). https://doi.org/10.1007/s00165-017-0437-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-017-0437-z