Theorem Prover Based Verification of TLA Systems
Ulrich Eickhoff, Peter Herrmann, Heiko Krumm
May, 1993

Abstract

TLA is an action-based linear-time temporal logic and supports the specifica-
tion and verification of concurrent systems. In general, verification is 
equivalent to the logical proof of implications between temporal formulas, 
which can be reduced to a set of predicate logic proofs. In this context 
our approach aims to the automation of verification processes by means of 
the utilization of automated predicate logic theorem provers. A tool named 
TOAST has been developed which accomplishes the reduction of temporal proofs 
to predicate logic proofs. For the ongoing predicate logic proofs, TOAST 
produces the input files and shell scripts, necessary to establish fully 
automated theorem prover runs. Presently the resolution-based theorem prover 
OTTER is applied. The paper outlines the approach and reports about the 
experiences gained so far.  Since we are interested in the support of
the development of practical distributed systems and communication systems, a
sliding window communication protocol serves as example.