Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Pinyin
i2Cantonese
i2Cangjie
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

ERSHOV

2009

Springer

2009

Springer

Abstract. Model programs are high-level behavioral speciﬁcations 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 speciﬁcation. 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.

Related Content

Added |
26 May 2010 |

Updated |
26 May 2010 |

Type |
Conference |

Year |
2009 |

Where |
ERSHOV |

Authors |
Margus Veanes, Nikolaj Bjørner |

Comments (0)