Abstract
We explain the rationale behind the design of the TLA + specification language, and we describe our experience using it and the TLC model checker in industrial applications–including the verification of multiprocessor memory designs at Intel. Based on this experience, we challenge some conventional wisdom about high-level specifications.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82(2), 253–284 (1991)
Ashcroft, E.A., Manna, Z.: Formalization of properties of parallel programs. In: Machine Intelligence, vol. 6. Edinburgh University Press, Edinburgh (1970)
Chandy, K.M., Misra, J.: Parallel Program Design. Addison-Wesley, Reading (1988)
Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panagaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)
Floyd, R.W.: Assigning meanings to programs. In: Proceedings of the Symposium on Applied Math., vol. 19, pp. 19–32. American Mathematical Society, Providence (1967)
Gafni, E., Lamport, L.: Disk paxos. To appear in Distributed Computing (2002)
Gharachorloo, K., Sharma, M., Steely, S., Van Doren, S.: Architecture and design of AlphaServer GS320. In: Gupta, A. (ed.) Proceedings of the Ninth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS IX), November 2000, pp. 13–24 (2000)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–583 (1969)
Holzmann, G.: The model checker spin. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Lam, S.S., Shankar, A.U.: Protocol verification via projections. IEEE Transactions on Software Engineering SE-10(4), 325–342 (1984)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering SE-3(2), 125–143 (1977)
Lamport, L.: An assertional correctness proof of a distributed algorithm. Science of Computer Programming 2(3), 175–206 (1982)
Lamport, L.: How to write a long formula. Formal Aspects of Computing 6, 580–584 (1994); First appeared as Research Report 119, Digital Equipment Corporation, Systems Research Center
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Lamport, L.: Composition: A way to make proofs harder. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 402–423. Springer, Heidelberg (1998)
Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2002); A link to an electronic copy can be found at http://lamport.org
Lamport, L., Matthews, J., Tuttle, M., Yu, Y.: Specifying and verifying systems with TLA+. In: Proceedings of the Tenth ACM SIGOPS European Workshop, Saint-Emilion, France, September 2002, pp. 45–48. INRIA (Institut National de Recherche en Informatique et en Automatique) (2002)
Lamport, L., Paulson, L.C.: Should your specification language be typed? ACM Transactions on Programming Languages and Systems 21(3), 502–526 (1999)
Lamport, L., Sharma, M., Tuttle, M., Yu, Y.: The wildfire verification challenge problem, At URL http://research.microsoft.com/users/lamport/tla/wildfire-challenge.html on the World Wide Web; It can also be found by searching the Web for the 24-letter string wildfirechallengeproblem
Owicki, S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM 19(5), 279–284 (1976)
Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems 4(3), 455–495 (1982)
Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering 21(2), 107–125 (1995)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on the Foundations of Computer Science, November 1977, pp. 46–57. IEEE, Los Alamitos (1977)
Tasiran, S., Yu, Y., Batson, B., Kreider, S.: Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor. In: Proceedings of the 3rd IEEE Workshop on Microprocessor Test and Verification, Common Challenges and Solutions. IEEE Computer Society, Los Alamitos (2002)
Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Batson, B., Lamport, L. (2003). High-Level Specifications: Lessons from Industry. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2002. Lecture Notes in Computer Science, vol 2852. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39656-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-39656-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20303-2
Online ISBN: 978-3-540-39656-7
eBook Packages: Springer Book Archive