Interface theories for concurrency and data |
| |
Authors: | Sebastian S Bauer Rolf Hennicker Martin Wirsing |
| |
Affiliation: | Institut für Informatik, Ludwig-Maximilians-Universität München, Germany |
| |
Abstract: | 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. |
| |
Keywords: | Component-based design Interface theory Modal input/output automata Pre- and postcondition Compositionality Refinement Compatibility |
本文献已被 ScienceDirect 等数据库收录! |