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

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureHoofdstukAcademicpeer review

3 Citaten (Scopus)
2 Downloads (Pure)

Samenvatting

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.

Originele taal-2Engels
TitelFundamental Approaches to Software Engineering
Plaats van productieDordrecht
UitgeverijSpringer
Pagina's383-400
Aantal pagina's18
ISBN van geprinte versie9783662496640
DOI's
StatusGepubliceerd - 2016
Evenement19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016) - Eindhoven, Nederland
Duur: 5 apr 20167 apr 2016
Congresnummer: 19

Publicatie series

NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9633
ISSN van geprinte versie03029743
ISSN van elektronische versie16113349

Congres

Congres19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016)
Verkorte titelFASE 2016
LandNederland
StadEindhoven
Periode5/04/167/04/16

Vingerafdruk Duik in de onderzoeksthema's van 'Verifying a verifier: on the formal correctness of an LTS transformation verification technique'. Samen vormen ze een unieke vingerafdruk.

Citeer dit