SIGNIFICANT EVENT TEMPORAL LOGIC - A METHOD FOR PROTOCOL SPECIFICATION AND VERIFICATION

In this paper we discuss the Significant Event Temporal Logic Techniqu e (SIGETL), a method for protocol specification and verification using a temporal logic axiomatic system. This technique is based on the ide a that the state and the behaviour of a module can be completely descr ibed by the sequence of the significant events with which the module c ommunicates with its environment till the present time. The behaviour of a module at any time is specified by simple temporal logic formulas , called transition axioms or properties of the module. Both, the safe ty and liveness properties of a module, as well as the global properti es of a system, can be proven from its axioms using the axiomatic temp oral logic system. As an example, we apply SIGETL to specify and verif y a simple data transfer protocol. The general correspondence between SIGETL and Estelle is also discussed. This allows an Estelle specifica tion to be easily translated into SIGETL for the purpose of verificati on.