Interface theories for concurrency and data

We present a compositional approach for specifying concurrent behavior of components with data states on the basis of interface theories. The dynamic aspects of a system are specified by modal input/output automata, whereas changing data states are specified by pre- and postconditions. The combinati...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2011-06, Vol.412 (28), p.3101-3121
Main Authors: Bauer, Sebastian S., Hennicker, Rolf, Wirsing, Martin
Format: Article
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Applied sciences
Automation
Compatibility
Component-based design
Compositionality
Computer science
control theory
systems
Computer simulation
Concretes
Dynamical systems
Dynamics
Exact sciences and technology
Formalism
Interface theory
Language theory and syntactical analysis
Mathematical models
Miscellaneous
Modal input/output automata
Pre- and postcondition
Refinement
Semantics
Software
Software engineering
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present a compositional approach for specifying concurrent behavior of components with data states on the basis of interface theories. The dynamic aspects of a system are specified by modal input/output automata, whereas changing data states are specified by pre- and postconditions. The combination of the two formalisms leads to our notion of modal input/output automata with data constraints (MIODs). In this setting we study refinement and behavioral compatibility of MIODs. We show that compatibility is preserved by refinement and that refinement is compositional w.r.t. synchronous composition, thus satisfying basic requirements of an interface theory. We propose a semantic foundation of interface specifications where any MIOD is equipped with a model-theoretic semantics describing the class of its correct implementation models. Implementation models are formalized in terms of guarded input/output transition systems and the correctness notion is based on a simulation relation between an MIOD and an implementation model which relates not only abstract and concrete control states but also (abstract) data constraints and concrete data states. We show that our approach is compositional in the sense that locally correct implementation models of compatible MIODs compose to globally correct implementations, thus ensuring independent implementability.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2011.04.007