Work-in-progress Assume-guarantee reasoning with ioco

L. Brandan Briones, Corina Pasareanu, Dimitra Giannakopoulou

    Research output: Book/ReportReportOther research output

    19 Downloads (Pure)

    Abstract

    This paper presents a combination between the assume-guarantee paradigm and the testing relation ioco. The assume-guarantee paradigm is a ”divide and conquer” technique that decomposes the verification of a system into smaller tasks that involve the verification of its components. The principal aspect of assume-guarantee reasoning is to consider each component separately, while taking into account assumptions about the context of the component. The testing relation ioco is a formal conformance relation for model-based testing that works on labeled transition systems. Our main result shows that, with certain restrictions, assume-guarantee reasoning can be applied in the context of ioco. This enables testing ioco-conformance of a system by testing its components separately.
    Original languageUndefined
    Number of pages8
    Publication statusPublished - 2004

    Keywords

    • IR-59908

    Cite this

    Brandan Briones, L., Pasareanu, C., & Giannakopoulou, D. (2004). Work-in-progress Assume-guarantee reasoning with ioco.