A technique for specifying and refining TCSP processes by using guards and liveness conditions

Abstract

A technique for the specification of TCSP processes based upon the concepts of guards and liveness rules is presented. It is shown how safety and liveness properties can be proved for processes specified in this way. A technique related to bisimulations is proposed to prove refinements correct. The technique is extended to handle the concealment of events in the implementing process. The refinement relation preserves the safety and liveness properties already proved for the specification. Parallel composition of specifications is also defined preserving the failures semantics. To illustrate the technique, an example is used throughout the paper.