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