TY - GEN
T1 - Property-driven benchmark generation
AU - Steffen, Bernhard
AU - Isberner, Malte
AU - Naujokat, Stefan
AU - Margaria, Tiziana
AU - Geske, Maren
PY - 2013
Y1 - 2013
N2 - We present a systematic approach to the automatic generation of platform-independent benchmarks of tailored complexity for evaluating verification tools for reactive systems. Key to this approach is a tool chain that essentially transforms a set of automatically generated LTL properties into source code for various formats, platforms, and competition scenarios via a sequence of property-preserving steps. These steps go through dedicated representations in terms of Büchi Automata, Mealy machines, Decision Diagram Models, Code Models, and finally the source code of the chosen scenario. The required transformations comprise LTL synthesis, model checking, property-oriented expansion, path condition extraction, theorem proving, SAT solving, and code motion. This combination allows us to address different communities via a growing set of programming languages, tailored sets of programming constructs, different notions of observation, and the full variety of LTL properties-ranging from mere reachability over general safety properties to arbitrary liveness properties. The paper illustrates the whole tool chain along accompanying examples, emphasizes the current state of development, and sketches the envisioned potential and impact of our approach.
AB - We present a systematic approach to the automatic generation of platform-independent benchmarks of tailored complexity for evaluating verification tools for reactive systems. Key to this approach is a tool chain that essentially transforms a set of automatically generated LTL properties into source code for various formats, platforms, and competition scenarios via a sequence of property-preserving steps. These steps go through dedicated representations in terms of Büchi Automata, Mealy machines, Decision Diagram Models, Code Models, and finally the source code of the chosen scenario. The required transformations comprise LTL synthesis, model checking, property-oriented expansion, path condition extraction, theorem proving, SAT solving, and code motion. This combination allows us to address different communities via a growing set of programming languages, tailored sets of programming constructs, different notions of observation, and the full variety of LTL properties-ranging from mere reachability over general safety properties to arbitrary liveness properties. The paper illustrates the whole tool chain along accompanying examples, emphasizes the current state of development, and sketches the envisioned potential and impact of our approach.
KW - Benchmark generation
KW - code motion
KW - LTL synthesis
KW - model checking
KW - path condition extraction
KW - property-oriented expansion
KW - SAT solving
KW - theorem proving
UR - http://www.scopus.com/inward/record.url?scp=84884925743&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39176-7_21
DO - 10.1007/978-3-642-39176-7_21
M3 - Conference contribution
AN - SCOPUS:84884925743
SN - 9783642391750
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 341
EP - 357
BT - Model Checking Software - 20th International Symposium, SPIN 2013, Proceedings
PB - Springer Verlag
T2 - 20th International Symposium on Model Checking Software, SPIN 2013
Y2 - 8 July 2013 through 9 July 2013
ER -