Abstract:
We explore the question of the composition of invariance
specifications in a context of concurrent and reactive systems.
Depending on how compositionality is stated and how invariants are
defined, invariance specifications may or may not be compositional.
This article first examines two classic forms of invariants and their
compositional properties. After pointing out what we see as
deficiencies of these two kinds of invariants, two new forms are defined
and shown to have useful compositional properties that the more
classic forms do not enjoy. The last form, in particular, is shown to
be well-suited to situations where none of the other three is adapted.
Michel Charpentier <
>
Last modified: Tue Apr 19 14:09:47 EDT 2005