Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers

Sebastian Gabmeyer; Martina Seidl

doi:10.1007/978-3-319-41135-4_6

Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers

Sebastian Gabmeyer
, Martina Seidl

Institute of Formal Models and Verification

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

Abstract

We present a novel symbolic bounded model checking approach to test reachability properties of model-driven software implementations. Given a concrete initial state of a software system, a type graph, and a set of graph transformations, which describe the system’s structure and its behavior, the system is tested against a reachability property that is expressed in terms of a graph constraint. Without any user intervention, our approach exploits state-of-the-art model checking technologies successfully used in hardware industry. The efficiency of our approach is demonstrated in two case studies.

Original language	German (Austria)
Title of host publication	Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016
Editors	Bernhard K. Aichernig, Carlo A. Furia
Publisher	Springer
Pages	94-111
Number of pages	18
Volume	9762
DOIs	https://doi.org/10.1007/978-3-319-41135-4_6
Publication status	Published - 2016

Publication series

Name	Lecture Notes in Computer Science (LNCS)

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

10.1007/978-3-319-41135-4_6

Cite this

Gabmeyer, S., & Seidl, M. (2016). Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers. In Bernhard K. Aichernig, Carlo A. Furia (Ed.), Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016 (Vol. 9762, pp. 94-111). (Lecture Notes in Computer Science (LNCS)). Springer. https://doi.org/10.1007/978-3-319-41135-4_6

Gabmeyer, Sebastian ; Seidl, Martina. / Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers. Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016. editor / Bernhard K. Aichernig, Carlo A. Furia. Vol. 9762 Springer, 2016. pp. 94-111 (Lecture Notes in Computer Science (LNCS)).

@inproceedings{70312d49969b4a59b9e903fc19a6542f,

title = "Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers",

abstract = "We present a novel symbolic bounded model checking approach to test reachability properties of model-driven software implementations. Given a concrete initial state of a software system, a type graph, and a set of graph transformations, which describe the system{\textquoteright}s structure and its behavior, the system is tested against a reachability property that is expressed in terms of a graph constraint. Without any user intervention, our approach exploits state-of-the-art model checking technologies successfully used in hardware industry. The efficiency of our approach is demonstrated in two case studies.",

author = "Sebastian Gabmeyer and Martina Seidl",

year = "2016",

doi = "10.1007/978-3-319-41135-4\_6",

language = "Deutsch ({\"O}sterreich)",

volume = "9762",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "94--111",

editor = "\{Bernhard K. Aichernig, Carlo A. Furia\}",

booktitle = "Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016",

}

Gabmeyer, S & Seidl, M 2016, Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers. in Bernhard K. Aichernig, Carlo A. Furia (ed.), Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016. vol. 9762, Lecture Notes in Computer Science (LNCS), Springer, pp. 94-111. https://doi.org/10.1007/978-3-319-41135-4_6

Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers. / Gabmeyer, Sebastian; Seidl, Martina.
Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016. ed. / Bernhard K. Aichernig, Carlo A. Furia. Vol. 9762 Springer, 2016. p. 94-111 (Lecture Notes in Computer Science (LNCS)).

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

TY - GEN

T1 - Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers

AU - Gabmeyer, Sebastian

AU - Seidl, Martina

PY - 2016

Y1 - 2016

N2 - We present a novel symbolic bounded model checking approach to test reachability properties of model-driven software implementations. Given a concrete initial state of a software system, a type graph, and a set of graph transformations, which describe the system’s structure and its behavior, the system is tested against a reachability property that is expressed in terms of a graph constraint. Without any user intervention, our approach exploits state-of-the-art model checking technologies successfully used in hardware industry. The efficiency of our approach is demonstrated in two case studies.

AB - We present a novel symbolic bounded model checking approach to test reachability properties of model-driven software implementations. Given a concrete initial state of a software system, a type graph, and a set of graph transformations, which describe the system’s structure and its behavior, the system is tested against a reachability property that is expressed in terms of a graph constraint. Without any user intervention, our approach exploits state-of-the-art model checking technologies successfully used in hardware industry. The efficiency of our approach is demonstrated in two case studies.

UR - https://www.scopus.com/pages/publications/84977552742

U2 - 10.1007/978-3-319-41135-4_6

DO - 10.1007/978-3-319-41135-4_6

M3 - Konferenzbeitrag

VL - 9762

T3 - Lecture Notes in Computer Science (LNCS)

SP - 94

EP - 111

BT - Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016

A2 - Bernhard K. Aichernig, Carlo A. Furia, null

PB - Springer

ER -

Gabmeyer S, Seidl M. Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers. In Bernhard K. Aichernig, Carlo A. Furia, editor, Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016. Vol. 9762. Springer. 2016. p. 94-111. (Lecture Notes in Computer Science (LNCS)). doi: 10.1007/978-3-319-41135-4_6

Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers

Abstract

Publication series

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this