More Web Proxy on the site http://driver.im/

research-article

Open access

A formal verification technique for behavioural model-to-model transformations

Authors:

Sander de Putter,

Anton WijsAuthors Info & Claims

Formal Aspects of Computing, Volume 30, Issue 1

Pages 3 - 43

https://doi.org/10.1007/s00165-017-0437-z

Published: 01 January 2018 Publication History

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 2ⁿ − 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.

References

References

[1]

Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, and Voisin L Rodin: an open toolset for modelling and reasoning in Event-B Softw Tools Technol Transf 2010 12 6 447-466

[2]

Amrani M, Combemale B, Lúcio L, Selim GMK, Dingel J, Le Traon Y, Vangheluwe H, and Cordy JR Formal verification techniques for model transformations: a tridimensional classification J Object Technol 2015 14 3 1-43

[3]

Abadi M and Lamport L The existence of refinement mappings Theor Comput Sci 1991 82 253-284

Digital Library

[4]

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

[5]

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

[6]

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

[7]

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

[8]

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

[9]

Bowen JP, Hinchey MG (2004) Formal methods. In: Computldbook, chapter 106. ACM, pp 106–1–106–25

[10]

Baier C and Katoen J-P Principles of model checking 2008 Cambridge MIT Press

Digital Library

[11]

Combemale B, Crégut X, Garoche P-L, and Thirioux X Essay on semantics definition in MDE: an instrumented approach for model verification J Softw 2009 4 9 943-958

[12]

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

[13]

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

[14]

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

[15]

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

[16]

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

[17]

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

[18]

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

[19]

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

[20]

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

[21]

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.

[22]

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

[23]

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

[24]

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

[25]

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

[26]

Kleppe A, Warmer J, Bast W (2005) MDA Explained: The Model Driven Architecture(TM): Practice and Promise. Addison-Wesley Professional

[27]

Lano K The B language and method, a guide to practical formal development 1996 New York Springer

[28]

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

[29]

Lang F and Mateescu R Partial model checking using networks of labelled transition systems and boolean equation systems Log Methods Comput Sci 2013 9 4 1-32

[30]

Luttik SP (1997) Description and formal specification of the link layer of P1394. Technical Report SEN-R9706, CWI

[31]

Mateescu R and Wijs AJ Property-dependent reductions adequate with divergence-sensitive branching bisimilarity Sci Comput Program 2014 96 3 354-376

Digital Library

[32]

National Institute of Standards and Technology (1999) Data encryption standard (DES). Federal information processing standards pp 46–3

[33]

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

[34]

Ploeger B (2009) Analysis of ACS using mCRL2. Technical Report 09-11, Eindhoven University of Technology

[35]

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

[36]

Romijn J (1999) Model checking a HAVi leader election protocol. Technical Report SEN-R9915, CWI

[37]

Ramalingam G and Reps T On the computational complexity of dynamic graph problems Theor Comput Sci 1996 158 233-277

Digital Library

[38]

Rahim LA, Whittle J (2013) A survey of approaches for verifying model transformations. Softw Syst Model pp 1–26.

[39]

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

[40]

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

[41]

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

[42]

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

[43]

Swamy GM (1996) Incremental methods for formal verification and logic synthesis. PhD thesis, University of California

[44]

van Glabbeek RJ and Weijland WP Branching time and abstraction in bisimulation semantics J ACM 1996 43 3 555-600

Digital Library

[45]

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

[46]

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

[47]

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

[48]

Wijs AJ, Fokkink WJ (2005) From

χ_{t}

to

μ

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

[49]

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

[50]

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

[51]

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

[52]

Winskel G A compositional proof system on a category of labelled transition systems Inf Comput 1990 87 1-2 2-57

Digital Library

Cited By

Chaki RWijs A(2022)Formally Characterizing the Effect of Model Transformations on System PropertiesFormal Aspects of Component Software10.1007/978-3-031-20872-0_3(39-58)Online publication date: 10-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-20872-0_3
Huisman MWijs AOortwijn W(2020)Towards verified construction of correct and optimised GPU softwareProceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs10.1145/3427761.3428344(10-14)Online publication date: 23-Jul-2020
https://dl.acm.org/doi/10.1145/3427761.3428344
Wijs AWiłkowski M(2019)Modular Indirect Push-Button Formal Verification of Multi-threaded Code GeneratorsSoftware Engineering and Formal Methods10.1007/978-3-030-30446-1_22(410-429)Online publication date: 18-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30446-1_22

Recommendations

A framework for model transformation verification
Abstract
A model transformation verification task may involve a number of different transformations, from one or more of a wide range of different model transformation languages, each transformation may have a particular transformation style, and there are ...
Model transformation verification using similarity and graph comparison algorithm

Regarding the software development, MDA (Model Driven Architecture) of OMG can be regarded as the concept of making an independently-designed model according to the development environment and language and reusing it according to the desired development ...
Formalised EMFTVM bytecode language for sound verification of model transformations

Model-driven engineering is an effective approach for addressing the full life cycle of software development. Model transformation is widely acknowledged as one of its central ingredients. With the increasing complexity of model transformations, it is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 30, Issue 1

Jan 2018

188 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© The Author(s) 2017.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 January 2018

Accepted: 08 September 2017

Received: 26 November 2016

Published in FAC Volume 30, Issue 1

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
54
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)5

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chaki RWijs A(2022)Formally Characterizing the Effect of Model Transformations on System PropertiesFormal Aspects of Component Software10.1007/978-3-031-20872-0_3(39-58)Online publication date: 10-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-20872-0_3
Huisman MWijs AOortwijn W(2020)Towards verified construction of correct and optimised GPU softwareProceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs10.1145/3427761.3428344(10-14)Online publication date: 23-Jul-2020
https://dl.acm.org/doi/10.1145/3427761.3428344
Wijs AWiłkowski M(2019)Modular Indirect Push-Button Formal Verification of Multi-threaded Code GeneratorsSoftware Engineering and Formal Methods10.1007/978-3-030-30446-1_22(410-429)Online publication date: 18-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30446-1_22

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents