Leslie Lamport
Abstract
The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple; its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician's toy; it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere.
- ABADI, M. AND LAMPORT, L. 1993. Conjoining specifications. Res. Rep. 118, Digital Equipment Corp., Systems Research Center, Palo Alto, Calif.Google Scholar
- ABADI, M. AND LAMPORT, L. 1992. An old-fashioned recipe for real time. Research Report 91, Digital Equipment Corp., Systems Research Center, Palo Alto, Calif.~Google Scholar
- ABADI, M. AND LAMPORT, L. 1991. The existence of refinement mappings. Theor. Comp. Sci. 82, 2 (May), 253-284. Google Scholar
- ALPERN, B. AND SCHNEIDER, F. B. 1985. Defining liveness. Inf. Process. Lett. 21, 4 (Oct.), 181-185.Google Scholar
- APT, K. R. 1981. Ten years of Hoare's logic: A survey--part one. ACM Trans. Programm. Lang. Syst. 3, 4 (Oct.), 431-483. Google Scholar
- APT, K. R. AND OLDEROG, E.-R. 1990. Verification of Sequential and Concurrent Programs. Springer-Verlag, New York. Google Scholar
- ASHCROFT, E. A. 1975. }Proving assertions about parallel programs. J. Comput. Syst. Sci. 10, 110-135.Google Scholar
- BURCH, J. R., CLARKE, E. M.~ MCMILLAN, K. L., DILL, D. L., AND HWANG, L. J. 1992. Symbolic model checking: 102o states and beyond, inf. Cornput. 98, 2 (June), 142-170. Google Scholar
- CHANDY, K. M. AND MISRA, J. 1988. Parallel Program Desipn. Addison-Wesley, Re ading, M ass. Google Scholar
- DE BAKKER, J. W., HUIZING, C., DE ROEVER, W. P., AND ROZENBERG, G. (Eds.) 1992. Real-Time: Theory in Practice, Lecture Notes in Computer Science, vol. 600. Proceedings of a REX Real-Time Workshop, Springer-Verlag, Berlin.Google Scholar
- DIJKSTRA, E. W. 1968. The structure of the "THE"-multiprogramming system. Comm. ACM 11, 5 (May), 341-346. Google Scholar
- DIJKSTRA, E. W. 1976. A Discipline of Programmin9. Prentice-Hall, Englewood Cliffs, N. J. Google Scholar
- ENCBERC, U., GRONNING, P., AND LAMPORT, L. 1992. Mechanical verification of concurrent systems with TLA. In Computer-Aided Verification, Lecture Notes in Computer Science, Proceedings of the 4th International Conference, CAV'92. Springer-Verlag, Berlin. Google Scholar
- FLON, L. AND SUZUKI, N. 1978. Consistent and complete proof rules for the total correctness of parallel programs. In Proceedings of 19th Annual Symposium on Foundations of Computer Science. IEEE, New York, 184-192.Google Scholar
- FLOYD, R. W. 1967. Assigning meanings to programs, in Proceedings of the Symposium on Applied Math. Vol. 19, American Mathematical Society, Providence, Rhode Island, 19-32.Google Scholar
- GARLAND, S. J. AND GUTTAG, J. V. 1989. An overview of LP, the Larch Prover. In Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, N. DERSHOWITZ, Ed. Lecture Notes on Computer Science, vol. 355. Springer-Verlag, New York, 137-151. Google Scholar
- HEHNER, E. C. R. 1984. Predicative programming. Comm. A CM 27, 2 (Feb.), 134-151. Google Scholar
- HOARE, C. 1969. An axiomatic basis for computer programming. Comm. A CM 12, 10 (Oct.), 576-583. Google Scholar
- KELLER, R. M. 1976. Formal verification of parallel programs. Comm. A CM 19, 7 (July), 371-384. Google Scholar
- LAM, S. S. AND SHANKAR, A. U. 1984. Protocol verification via projections. IEEE Trans. Softw. Eng. SE-IO, 4 (July), 325-342.Google Scholar
- LAMPORT, L. 1993. Hybrid systems in TLA+. In Hybmd Systems, R. L. GRoss- MAN, A. NERODE, A. P. RAVN, AND U. RISCHEL, Eds. Lecture Notes m Computer Science, vol. 736. Springer-Verlag, Berlin, 77-102. Google Scholar
- LAMPORT, L. 1983a. Specifying concurrent program modules. A CM Trans. Program. Lang. Syst 5, 2 (April), 190-222. Google Scholar
- LAMPORT, L. 1983b. What good is temporal logic. In Information Processing 83: Proceedings of the IFIP 9th World Congress, R. E. A. MASON, Ed. North-Holland, Amsterdam, 657-668.Google Scholar
- LAMPORT, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2 (Mar.), 125-143.Google Scholar
- LE~SENR~NG, A. C. 1969. Mathematical Logic and Hilbert's e-Symbol. Gordon and Breach, New York.Google Scholar
- LIPTON, R. J. 1975. Reduction: A method of proving properties of parallel programs. Comm. ACM 18, 12 (Dec.), 717-721. Google Scholar
- LYNCH, N. AND TUTTLE, M. 1987. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6th Symposium on the Princzples of Distributed Computing, ACM, New York, 137-151. Google Scholar
- MANNA, Z. AND PNUELI, A. 1991. The Temporal Logzc of Reactwe and Concurrent Systems. Springer-Vertag, New York. Google Scholar
- MISRA, J. 1990. Specifying concurrent objects as communicating processes. Scz. Comput. Program. 1~, 2-3, 159-184. Google Scholar
- OWICKI, S. 1975. Axiomatic proof techniques for parallel programs. Ph. D. thesis, Cornell University, Ithaca N. Y. Google Scholar
- PNUELI, A. 1979. The temporal semantics of concurrent programs. In Semantics of Concurrent Computation, G. KAHN, Ed, Lecture Notes in Co~np~ter Science, vol. 70. Springer-Verlag, New York, 1-20. Google Scholar
- PNUELI, A. 1977. The temporal logic of programs. In Procee&ngs of the 18th Annual Symposium on the Foundations of Computer Science, IEEE, New York, 46-57.Google Scholar
- SCHROEDER~ M. D., BIRRELL, A. D., BURROWS, M., MURRAY, H., NEED- HAM, R. M., RODEHEFFER, T. L., SATTERTHWAITE, E. H., AND THACKER, C. P. 1990. Autonet: A high-speed, self-configuring local area network using point-to-point links. Res. Rep. 59, Digital Equipment Corporation, Systems Research Center, Palo Alto, Calif.Google Scholar
- SHANKAR, A. U. AND LAM, S. S. 1984. Time-dependent communication protocols. In Principles of Communication and Networking Protocols, S. S. LAM, Ed. IEEE Computer Society Press, Los Alamitos, Calif., 504- 519.Google Scholar
Index Terms
- The temporal logic of actions
Recommendations
Composing specifications
A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle because a component need behave correctly ...
Conjoining specifications
We show how to specify components of concurrent systems. The specification of a system is the conjunction of its components' specifications. Properties of the system are proved by reasoning about its components. We consider both the decomposition of a ...
A formal approach for the development of reactive systems
Context: This paper deals with the development and verification of liveness properties on reactive systems using the Event-B method. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA^+ to ...
Comments