A Synthesis Rule for Concurrent Systems

Concurrent (hardware and software) systems can become extremely complex due to the existence of multiple loci of control. Posteriori analysis of such systems is very difficult. This paper presents a systematic bottom-up modular approach to synthesis. The synthesis procedure at each stage yields all invariants (of a certain kind) of the system. These invariants can be used as an aid to proving certain properties of the system such as boundedness, conservativeness, mutual exclusion, absence of deadlock, etc. The use of the synthesis rule and the utility of the invariants are illustrated by examples.