Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
An SMT Approach to Bounded Reachability Analysis of Model Programs

Margus Veanes, Nikolaj Bjørner, and Alexander Raschke

Abstract

Model programs represent transition systems that are used to specify expected behavior of systems at a high level of abstraction. The main application area is application-level network protocols or protocol-like aspects of software systems. Model programs typically use abstract data types such as sets and maps, and comprehensions to express complex state updates. Such models are mainly used in model-based testing as inputs for test case generation and as oracles during conformance testing. Correctness assumptions about the model itself are usually expressed through state invariants. An important problem is to validate the model prior to its use in the above-mentioned contexts. We introduce a technique of using Satisfiability Modulo Theories or SMT to perform bounded reachability analysis of a fragment of model programs. We use the Z3 solver for our implementation and benchmarks, and we use AsmL as the modeling language. The translation from a model program into a verification condition of Z3 is incremental and involves selective quantifier instantiation of quantifiers that result from the comprehension expressions.

Details

Publication typeInproceedings
Published inFORTE'08
Pages53-68
Volume5048
SeriesLNCS
PublisherSpringer Verlag
> Publications > An SMT Approach to Bounded Reachability Analysis of Model Programs