Symbolic Bounded Conformance Checking of Model Programs

Margus Veanes and Nikolaj Bjorner

June 2009

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.

Publication type | Inproceedings |

Published in | Perspectives of System Informatics (PSI'09) |

Pages | 388-400 |

Volume | 5947 |

Series | LNCS |

Publisher | Springer Verlag |

Margus Veanes and Nikolaj Bjorner. Symbolic Bounded Conformance Checking of Model Programs, Microsoft, 14 March 2009.

- Modeling Software: From Theory to Practice
- Qex: Symbolic SQL Query Explorer
- The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification

> Publications > Symbolic Bounded Conformance Checking of Model Programs