SPECIFICATION OF COMMUNICATION SYSTEMS WITH TEMPORAL LOGIC  

作　　者：周巢尘 

机构地区：[1]Institute of Software, Academia Sinica, Beijing 100080, PRC

出　　处：《Science China Mathematics》1990年第4期486-502,共17页中国科学：数学（英文版）

基　　金：Project supported by the National Natural Science Foundation of China

摘　　要：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.

关 键 词：FORMAL SPECIFICATION distributed PROGRAMMING PROGRAMMING LOGIC TEMPORAL LOGIC COMMUNICATING process. 

分 类 号：N[自然科学总论]