摘要
A temporal logic for specifying the external behaviours of systems is introduced. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, i.e. intending to do a communication, passing a message, or being closed. Auxiliary variables are recommended to describe system states by assembling channels’ states. Safety, termination, liveness and fairness can then be expressed in the logic. Specifications employing the 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 the internal structure and the protocol of the system, called the protocol specification. A set of inference rules are also presented for proving that a system of certain protocol specification satisfies its behaviour specification. The validity of the rules is given by defining a temporal model of the CSP notation.
A temporal logic for specifying the external behaviours of systems is introduced. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, i.e. intending to do a communication, passing a message, or being closed. Auxiliary variables are recommended to describe system states by assembling channels' states. Safety, termination, liveness and fairness can then be expressed in the logic. Specifications employing the 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 the internal structure and the protocol of the system, called the protocol specification. A set of inference rules are also presented for proving that a system of certain protocol specification satisfies its behaviour specification. The validity of the rules is given by defining a temporal model of the CSP notation.
基金
Project supported by the National Natural Science Foundation of China
