Specifying and verifying systems with TLA+

ABSTRACT

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.

REFERENCES

• 1: Alpha Architecture Committee. Alpha Architecture Reference Manual. Digital Press, Boston, third edition, 1998.
• 2: E. Gafni and L. Lamport. Disk paxos. Technical Report 163, Compaq Systems Research Center, July 2000. To appear in Distributed Computing. Currently available on the web at http://gatekeeper.dec.com/pub/DEC/SRC/research-reports/abstracts/src-rr% -163. html.
• 3: Kourosh Gharachorloo , Madhu Sharma , Simon Steely , Stephen Van Doren, Architecture and design of AlphaServer GS320, Proceedings of the ninth international conference on Architectural support for programming languages and operating systems, p.13-24, November 2000, Cambridge, Massachusetts, United States
• 4: L. Lamport. TLA---temporal logic of actions. A web page, a link to which can be found at URL http://lamport.org. The page can also be found by searching the Web for the 21-letter string formed by concatenating uid and lamporttlahomepage.
• 5: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 6: L. Lamport. How to write a proof. American Mathematical Monthly, 102(7):600--608, August-September 1995.
• 7: L. Lamport. Specifying Systems. Addison-Wesley, Boston, 2002.
• 8: L. Lamport, M. Sharma, M. Tuttle, and Y. Yu. The wildfire verification challenge problem. At URL http://www.research.compaq.com/SRC/tla/wildfire-challenge.html on the World Wide Web. It can also be found by searching the Web for the 24-letter string wild fire challenge problem.
• 9: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 10: S. Tasiran, Y. Yu, B. Batson, and S. Kreider. Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor. In In Proceedings of the 3rd IEEE Workshop on Microprocessor Test and Verification, Common Challenges and Solutions. IEEE Computer Society, 2002. To appear as an HP technical report.
• 11: Yuan Yu , Panagiotis Manolios , Leslie Lamport, Model Checking TLA+ Specifications, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.54-66, September 27-29, 1999