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 language | English |
---|---|
Title of host publication | 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) |
Editors | N. Piterman, S.A. Smolka |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 565-579 |
ISBN (Print) | 978-3-642-36741-0 |
DOIs | |
Publication status | Published - 2013 |
Event | 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013) - Rome, Italy Duration: 18 Mar 2013 → 21 Mar 2013 Conference number: 19 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Volume | 7795 |
ISSN (Print) | 0302-9743 |
Conference
Conference | 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013) |
---|---|
Abbreviated title | TACAS 2013 |
Country/Territory | Italy |
City | Rome |
Period | 18/03/13 → 21/03/13 |
Other | Conference held as part of the 16th European Joint Conferences on Theory and Practice of Software (ETAPS 2013) |