Compositional refinement of interactive systems

Research output: Contribution to journalArticlepeer-review

49 Scopus citations

Abstract

We introduce a method to describe systems and their components by functional specification techniques. We define notions of interface and interaction refinement for interactive systems and their components. These notions of refinement allow us to change both the syntactic (the number of channels and sorts of messages at the channels) and the semantic interface (causality flow between messages and interaction granularity) of an interactive system component. We prove that these notions of refinement are compositional with respect to sequential and parallel composition of system components, communication feedback and recursive declarations of system components. According to these proofs, refinements of networks can be accomplished in a modular way by refining their components. We generalize the notions of refinement to refining contexts. Finally, full abstraction for specifications is defined, and compositionality with respect to this abstraction is shown, too.

Original languageEnglish
Pages (from-to)850-891
Number of pages42
JournalJournal of the ACM
Volume44
Issue number6
DOIs
StatePublished - Nov 1997

Keywords

  • Design
  • Interactive systems
  • Refinement
  • Specification
  • Verification

Fingerprint

Dive into the research topics of 'Compositional refinement of interactive systems'. Together they form a unique fingerprint.

Cite this