Efficient property preservation checking of model refinements

A.J. Wijs, L.J.P. Engelen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

16 Citations (Scopus)

Abstract

In model-driven software development, models and model refinements are used to create software. To automatically generate correct software from abstract models by means of model refinement, desirable properties of the initial models must be preserved. We propose an explicit-state model checking technique to determine whether refinements are property preserving. We use networks of labelled transition systems (LTSs) to represent models with concurrent components, and formalise refinements as systems of LTS transformation rules. Property preservation checking involves determining how a rule system relates to an input network, and checking bisimilarity between behaviour subjected to transformation and the corresponding behaviour after transformation. In this way, one avoids generating the entire LTS of the new model. Experimental results demonstrate speedups of several orders of magnitude.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems (19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings)
EditorsN. Piterman, S.A. Smolka
Place of PublicationBerlin
PublisherSpringer
Pages565-579
ISBN (Print)978-3-642-36741-0
DOIs
Publication statusPublished - 2013
Event19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013) - Rome, Italy
Duration: 18 Mar 201321 Mar 2013
Conference number: 19

Publication series

NameLecture Notes in Computer Science
Volume7795
ISSN (Print)0302-9743

Conference

Conference19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013)
Abbreviated titleTACAS 2013
CountryItaly
CityRome
Period18/03/1321/03/13
OtherConference held as part of the 16th European Joint Conferences on Theory and Practice of Software (ETAPS 2013)

Fingerprint Dive into the research topics of 'Efficient property preservation checking of model refinements'. Together they form a unique fingerprint.

  • Cite this

    Wijs, A. J., & Engelen, L. J. P. (2013). Efficient property preservation checking of model refinements. In N. Piterman, & S. A. Smolka (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings) (pp. 565-579). (Lecture Notes in Computer Science; Vol. 7795). Berlin: Springer. https://doi.org/10.1007/978-3-642-36742-7_41