- Abstract:
-
The compositional approach reduces the verification of a property P of a system C(S1, . . .,Sn) assembled from the components S1, . . ., Sn to the verification of other properties P1, . . ., Pn on the components of the system. There are two parameters here: (1) The specification language SPEC in which properties are formulated. (2) The collection of operations OP by which a complex system can be assembled from its components.
The ideal dream of compositionality (Composition Theorem) is to give an algorithm which for every formula P of SPEC and every n-ary operator C in OP will construct formulas P1, . . .,Pn such that C(S1, . . . , Sn) satisfies P iff S1 satisfies P1, S2 satisfies P2, . . . and Sn satisfies Pn.
We will show that the composition theorem is realizable when the specification language SPEC is the multi-modal logic and the set of operations OP consists of a wide variety of product (``parallel composition'') operators. On the other hand, we will show if SPEC can express ``there is a path such that all the nodes of the path have a property p'', then (even non-algorithmic version of) the composition theorem fails for very simple parallel operators.
- Copyright:
- 2001 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @Misc{EDI-INF-RR-0035,
- author = {
Alexander Rabinovich
},
- title = {On Compositional Method and its Limitations},
- year = 2001,
- month = {Jan},
- }
|
