Assume-guarantee Reasoning with ioco Testing Relation

TitleAssume-guarantee Reasoning with ioco Testing Relation
Publication TypeConference Paper
Year of Publication2010
AuthorsBrandán Briones, L
Conference NameProceedings of the 22nd IFIP International Conference on Testing Software and Systems: Short Papers
ISBN Number978-2-89522-136-4
AbstractCompositional reasoning is typically based on assume-gua- rantee reasoning principles, which consider each component separately and take into account assumptions about the context of the component. This paper presents a combination of the assume-guarantee paradigm and ioco, a formal conformance relation for model-based testing that works on input-output transition systems (IOTS). We show that, un- der certain restrictions, assume-guarantee reasoning can be applied in the ioco context, enabling to check ioco-conformance by testing com- ponents’ system separately. We improve on previous results, where spec- ifications are required to be given as components, allowing the specifica- tions to be complete systems. Moreover, we prove that assume-guarantee reasoning can also be applied even when hiding internal communication between components.
URLhttp://crim.ca/Publications/2010/documents/plein_texte/ASD_PetA_al_201010_ICTSS_sp.pdf
PDF (Full text):