Verifying a verifier: on the formal correctness of an LTS transformation verification technique

S.M.J. de Putter, A.J. Wijs

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

3 Citations (Scopus)
2 Downloads (Pure)

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 languageEnglish
Title of host publicationFundamental Approaches to Software Engineering
Place of PublicationDordrecht
PublisherSpringer
Pages383-400
Number of pages18
ISBN (Print)9783662496640
DOIs
Publication statusPublished - 2016
Event19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016) - Eindhoven, Netherlands
Duration: 5 Apr 20167 Apr 2016
Conference number: 19

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9633
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016)
Abbreviated titleFASE 2016
CountryNetherlands
CityEindhoven
Period5/04/167/04/16
OtherConference held as part of the 19th European Joint Conferences on Theory and Practice of Software (ETAPS 2016)

Fingerprint Dive into the research topics of 'Verifying a verifier: on the formal correctness of an LTS transformation verification technique'. Together they form a unique fingerprint.

  • Cite this

    de Putter, S. M. J., & Wijs, A. J. (2016). Verifying a verifier: on the formal correctness of an LTS transformation verification technique. In Fundamental Approaches to Software Engineering (pp. 383-400). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9633). Springer. https://doi.org/10.1007/978-3-662-49665-7_23