An Interface Theory for Input/Output Automata

Research output: Book/ReportReportResearch

502 Downloads (Pure)

Abstract

Building on the theory of interface automata by de~Alfaro and
Henzinger we design an interface language for Lynch's Input/Output
Automata, a popular formalism used in the development of distributed
asynchronous systems, not addressed by previous interface research.
We introduce an explicit separation of assumptions from guarantees
not yet seen in other behavioral interface theories. Moreover we
derive the composition operator systematically and formally,
guaranteeing that the resulting compositions are always the weakest
in the sense of assumptions, and the strongest in the sense of
guarantees. We also present a method for solving systems of
relativized behavioral inequalities as used in our setup and draw a
formal correspondence between our work and interface
automata. Proofs are provided in an appendix.
Original languageEnglish
Place of PublicationÅrhus
PublisherBRICS
EditionRS-06-10
Number of pages40
Publication statusPublished - 2006

Fingerprint Dive into the research topics of 'An Interface Theory for Input/Output Automata'. Together they form a unique fingerprint.

Cite this