Compositional theories based on an operational semantics of contexts

Abstract

For the verification of large systems in general and parallel systems in particular, it is essential that the proof method used is compositional in order to avoid a combinatorial explosion of the verification. That is, the method must allow us to decompose the problem of correctness for a complex system into similar correctness problems for the components of the system. Compositionality requires a suitable relationship between the constructions available for building systems and the notion of correctness between systems and specifications. In fact, as we show in the paper, compositional proof methods may be classified in a number of ways; in particular classes well-suited for top-down and bottom-up development are identified. The main purpose of this paper is to demonstrate that compositionality in many cases may be achieved though a new operational understanding of the constructions (or contexts) used for building systems. The operational model we propose is that of action transducers; i.e. a construction is semantically viewed as an object transforming actions of its inner components into actions for the surrounding environment. In particular we demonstrate how to describe the constructions of CCS in this model. We present three proof methods (bisimulation, relative hisimulation and recursive modal logic), and show that the operational semantics of contexts in all cases leads to compositionality results.