Damm, W. and Josko, B. and Hungar, H. and Pnueli, A.
Compositionality: The Significant Difference; International Symposium COMPOS '97
This paper presents a reference semantics for a verification tool currently under development allowing to verify temporal properties of embedded control systems modelled using the STATEMATE system. The semantics reported differs from others reported in the literature by faithfully modelling the semantics as supported in the STATEMATE simulation tool. It differs from the recent paper by Harel and Naamad by providing a compositional semantics, a prerequisite for the support of compositional verification methods, and by the degree of mathematical rigour. We use a variant of synchronous transition systems introduced by Manna and Pnueli as base model for our semantics.
The STATEMATE modelling language constructs covered in this paper are Activity charts, modelling the functional decomposition of a design into subunits called activities as well as the information flow between these, and Statecharts, modelling reactive behaviour using the well established approach of hierarchically organized state-machines. We strive for a verification approach which is compositional w.r.t. the decomposition of systems into subsystems. This will allow activities of reasonable complexity to be verified using symbolic model checking.
Larger activities will be verified on the basis of proof-systems relating properties of individual activities to properties of compound activities, using the well known assumption commitment paradigm. A key topic for this paper is the construction of so called compositional models, which are rich enough to model the STATEMATE parallel composition by intersection of the infinite traces generated by the components of the parallel composition. Roughly, compositional models have to provide room for padding arbitrary (but still legal) environment interactions into computations of a component. Alternatively, the construction of compositional models can be phrased as a requirement on the model to support a sufficiently rich class of observables for assumption-commitment style reasoning to be complete. In this sense, this paper derives the set of atomic propositions included as observables in the assumption-commitment style temporal logic supported by the verification tool.
The richness of the STATEMATE modelling languages forbids a complete treatment within such a formal semantics. While Harel and Naamad elaborate in a detailed fashion the construction of compound transitions from transition segments, we take this as given in this paper. We also abstract from the concrete syntax of action annotations, but keep them rich enough to show how all the associated intricacies can be handled formally.