Specifying communicating systems with temporal logic

Abstract

We introduce a temporal logic for specifying external behaviour of systems. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, intending to do a communication, passing a message, or being closed. Auxiliary variable is recommended to describe system state by assembling the channels' states. Safety, termination, liveness and fairness properties can then be expressed in the logic, Specifications employing that logic will benefit from the compositionality: the conjunction of specifications of subsystems makes a specification of the whole system. Meanwhile a CSP-like notation is suggested to specify internal structure and protocol of system, called protocol specification. A set of inference rules is also presented for proving a system of certain protocol specification to satisfy its behaviour specification. The validity of the rules is given by defining a temporal model of the CSP notation.