In this paper we intend to provide the theoretical foundation for a top-down design methodology for reactive systems. The problem under consideration is that of compositionality in the following sense:What properties must the components of a combined system satisfy, in order that the overall system satisfies a given specification.We would like the properties required to be as weak as possible, in order not to limit the choice for further development. Also, we want these properties to be decomposable in the sense that they can be expressed as separate properties required of the individual components. To allow a general investigation of this problem, a new operational semantics of contexts in the form of action transducers is given. As specification language, a version of Hennessy-Milner Logic extended with recursion is used.
展开▼
