Specifying and verifying systems with TLA+

Proceedings of the Tenth ACM SIGOPS European Workshop |

Published by Association for Computing Machinery, Inc. | Organized by INRIA (Institut National de Recherche en Informatique et en Automatique)

Publication

TLA+ is a high-level specification language that has been used to specify and check the correctness of several hardware protocols. We expect that it can also be used to specify and check concurrent algorithms and protocols for software systems.

This describes our experience at DEC/Compaq using TLA+ and the TLC model checker on several systems, mainly cache-coherence protocols. It is shorter than, and more up-to-date than [128].