×

zbMATH — the first resource for mathematics

Compositionality through an operational semantics of contexts. (English) Zbl 0738.68056
Summary: 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.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
03B45 Modal logic (including the logic of norms)
PDF BibTeX XML Cite
Full Text: DOI