Sebastian Gabmeyer, Martina Seidl,
"Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers"
, in Bernhard K. Aichernig, Carlo A. Furia: Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016, Serie Lecture Notes in Computer Science (LNCS), Vol. 9762, Springer, Seite(n) 94-111, 2016
Original Titel:
Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers
Sprache des Titels:
Deutsch
Original Buchtitel:
Tests and Proofs - Proc. of the 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016
Englische Kurzfassung:
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.
Forschungs-