Abstract:
We explore the question of the composition of invariance
specifications in a context of formal methods applied to concurrent
and reactive systems. Depending on how compositionality is stated and
how invariants are defined, invariance specifications may or may not
be compositional. This paper examines three classic forms of
invariants and their compositional properties. After pointing out
what we see as deficiencies of these kinds of invariants, a new fourth
form is defined and shown to have useful compositional properties that
the more classic forms do not enjoy.
Keywords: formal specification, temporal logic,
compositional verification, invariants.
Michel Charpentier <>
Last modified: Mon May 5 17:22:04 EDT 2003