Verifying a verifier: on the formal correctness of an LTS transformation verification technique. (English) Zbl 1378.68114

Stevens, Perdita (ed.) et al., Fundamental approaches to software engineering. 19th international conference, FASE 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49664-0/pbk; 978-3-662-49665-7/ebook). Lecture Notes in Computer Science 9633, 383-400 (2016).
Summary: 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.
For the entire collection see [Zbl 1333.68018].


68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)


Full Text: DOI