Compositional assume-guarantee reasoning for input/output component theories

  • Chilton C
  • Jonsson B
  • Kwiatkowska M
  • 6

    Readers

    Mendeley users who have this article in their library.
  • 7

    Citations

    Citations of this article.

Abstract

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. © 2014 Elsevier B.V.

Author-supplied keywords

  • Assume-guarantee
  • Contracts
  • Interface automata
  • Quotient
  • Substitutivity

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Authors

  • Chris Chilton

  • Bengt Jonsson

  • Marta Kwiatkowska

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free