Symbolic Bounded Conformance Checking of Model Programs

13 years 5 days ago
Symbolic Bounded Conformance Checking of Model Programs
Abstract. Model programs are high-level behavioral specifications typically representing Abstract State Machines or ASMs. Conformance checking of model programs is the problem of deciding if the set of traces allowed by one model program forms a subset of the set of traces allowed by another model program. This is a foundational problem in the context of model-based testing, where one model program corresponds to an implementation and the other one to its specification. Here model programs are described using the ASM language AsmL. We assume a background T containing linear arithmetic, sets, and tuples. We introduce the Bounded Conformance Checking problem or BCC as a special case of the conformance checking problem when the length of traces is bounded and provide a mapping of BCC to a theorem proving problem in T . BCC is shown to be highly undecidable in the general case but decidable for a class of model programs that are common in practice.
Margus Veanes, Nikolaj Bjørner
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Authors Margus Veanes, Nikolaj Bjørner
Comments (0)