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 - Conference proceedings
SN - 9783319411347
VL - 9762
T3 - Lecture Notes in Computer Science
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 - Aichernig, Bernhard K.
A2 - Furia, Carlo A.
PB - Springer
ER -