Abstract
Over the years, various formal methods have been proposed and further developed to determine the functional correctness of models of concurrent systems. Some of these have been designed for application in a model-driven development workflow, in which model transformations are used to incrementally transform initial abstract models into concrete models containing all relevant details. In this paper, we consider an existing formal verification technique to determine that formalisations of such transformations are guaranteed to preserve functional properties, regardless of the models they are applied on. We present our findings after having formally verified this technique using the Coq theorem prover. It turns out that in some cases the technique is not correct. We explain why, and propose an updated technique in which these issues have been fixed.
Original language | English |
---|---|
Title of host publication | Fundamental Approaches to Software Engineering |
Place of Publication | Dordrecht |
Publisher | Springer |
Pages | 383-400 |
Number of pages | 18 |
ISBN (Print) | 9783662496640 |
DOIs | |
Publication status | Published - 2016 |
Event | 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016) - Eindhoven, Netherlands Duration: 5 Apr 2016 → 7 Apr 2016 Conference number: 19 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 9633 |
ISSN (Print) | 03029743 |
ISSN (Electronic) | 16113349 |
Conference
Conference | 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016) |
---|---|
Abbreviated title | FASE 2016 |
Country/Territory | Netherlands |
City | Eindhoven |
Period | 5/04/16 → 7/04/16 |
Other | Conference held as part of the 19th European Joint Conferences on Theory and Practice of Software (ETAPS 2016) |