Technical Reports

The ICICS/CS Reading Room


UBC CS TR-88-03 Summary

Protocol Specification and Verification using the Significant Event Temporal Logic, January 1988 George K. Tsiknis and Son T. Vuong

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.


If you have any questions or comments regarding this page please send mail to help@cs.ubc.ca.