Compositional assume–guarantee reasoning for input/output component theories
2014 (English)In: Science of Computer Programming, ISSN 0167-6423, Vol. 91, 115-137 p.Article in journal (Refereed) Published
We formulate a sound and complete assume-guarantee framework for reasoning compositionally about components modelled as a variant of interface automata. The specification of a component, which expresses both safety and progress properties of input and output interactions with the environment, is characterised by finite traces. The framework supports dynamic reasoning about components and specifications, and includes rules for parallel composition, logical conjunction and disjunction corresponding to independent development, and quotient for incremental synthesis. Practical applicability of the framework is demonstrated through a link layer protocol case study.
Place, publisher, year, edition, pages
2014. Vol. 91, 115-137 p.
IdentifiersURN: urn:nbn:se:uu:diva-216474DOI: 10.1016/j.scico.2013.12.010ISI: 000338401300006OAI: oai:DiVA.org:uu-216474DiVA: diva2:689957
9th International Symposium on Formal Aspects of Component Software (FACS), Mountain View, CA, September 12-14, 2012