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

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

doi:10.1007/978-3-662-49665-7_23

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

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

Software Engineering and Technology

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

4 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 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	https://doi.org/10.1007/978-3-662-49665-7_23
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)

Access to Document

10.1007/978-3-662-49665-7_23

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

@inbook{f57f2f1e861948a18eb5742af3a1a29e,

title = "Verifying a verifier: on the formal correctness of an LTS transformation verification technique",

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.",

author = "{de Putter}, S.M.J. and A.J. Wijs",

year = "2016",

doi = "10.1007/978-3-662-49665-7_23",

language = "English",

isbn = "9783662496640",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "383--400",

booktitle = "Fundamental Approaches to Software Engineering",

address = "Germany",

note = "19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016), FASE 2016 ; Conference date: 05-04-2016 Through 07-04-2016",

}

de Putter, SMJ & Wijs, AJ 2016, Verifying a verifier: on the formal correctness of an LTS transformation verification technique. in Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9633, Springer, Dordrecht, pp. 383-400, 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016), Eindhoven, Netherlands, 5/04/16. https://doi.org/10.1007/978-3-662-49665-7_23

Verifying a verifier : on the formal correctness of an LTS transformation verification technique. / de Putter, S.M.J.; Wijs, A.J.

Fundamental Approaches to Software Engineering. Dordrecht : Springer, 2016. p. 383-400 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9633).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Verifying a verifier

T2 - 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016)

AU - de Putter, S.M.J.

AU - Wijs, A.J.

N1 - Conference code: 19

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84961711998&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-49665-7_23

DO - 10.1007/978-3-662-49665-7_23

M3 - Chapter

AN - SCOPUS:84961711998

SN - 9783662496640

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 383

EP - 400

BT - Fundamental Approaches to Software Engineering

PB - Springer

CY - Dordrecht

Y2 - 5 April 2016 through 7 April 2016

ER -

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

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this