Protocol Specification and Verification using the Significant Event Temporal Logic

George K. Tsiknis and Son T. Vuong
Publishing date
January 1988
In this report we discuss the Significant Event Temporal Logic specification technique (SIGETL), a method for protocol specification and verification using a temporal logic axiomatic system. This technique is based on the idea that the state and the behaviour of a module can be completely described by the sequence of the significant events with which the module was involved in communicating 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 safety and liveness properties of a module, as well as the global properties of a system, can be proven from its axioms using the axiomatic temporal logic system. As an example, we apply SIGETL to specify and verify a simple data transfer protocol. The general correspondence between SIGETL and ESTELLE FDT is also discussed.