The temporal logic of actions
Tóm tắt
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.
Từ khóa
Tài liệu tham khảo
ABADI , M. AND LAMPORT , L. 1993. Conjoining specifications. Res. Rep. 118 , Digital Equipment Corp., Systems Research Center , Palo Alto, Calif. ABADI, M. AND LAMPORT, L. 1993. Conjoining specifications. Res. Rep. 118, Digital Equipment Corp., Systems Research Center, Palo Alto, Calif.
ALPERN , B. AND SCHNEIDER , F. B. 1985 . Defining liveness . Inf. Process. Lett. 21 , 4 (Oct.), 181-185. ALPERN, B. AND SCHNEIDER, F. B. 1985. Defining liveness. Inf. Process. Lett. 21, 4 (Oct.), 181-185.
APT , K. R. AND OLDEROG , E.-R. 1990. Verification of Sequential and Concurrent Programs . Springer-Verlag , New York . APT, K. R. AND OLDEROG, E.-R. 1990. Verification of Sequential and Concurrent Programs. Springer-Verlag, New York.
ASHCROFT , E. A. 1975 . }Proving assertions about parallel programs . J. Comput. Syst. Sci. 10 , 110 - 135 . ASHCROFT, E. A. 1975. }Proving assertions about parallel programs. J. Comput. Syst. Sci. 10, 110-135.
CHANDY , K. M. AND MISRA , J. 1988. Parallel Program Desipn . Addison-Wesley , Re ading, M ass. CHANDY, K. M. AND MISRA, J. 1988. Parallel Program Desipn. Addison-Wesley, Re ading, M ass.
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. 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.
DIJKSTRA , E. W. 1976. A Discipline of Programmin9 . Prentice-Hall , Englewood Cliffs, N. J. DIJKSTRA, E. W. 1976. A Discipline of Programmin9. Prentice-Hall, Englewood Cliffs, N. J.
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. 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.
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 . 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.
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 . 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.
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 . 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.
LAM , S. S. AND SHANKAR , A. U. 1984 . Protocol verification via projections . IEEE Trans. Softw. Eng. SE-IO , 4 ( July ), 325 - 342 . LAM, S. S. AND SHANKAR, A. U. 1984. Protocol verification via projections. IEEE Trans. Softw. Eng. SE-IO, 4 (July), 325-342.
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. 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.
LAMPORT , L. 1983 b. 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 . 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.
LAMPORT , L. 1977 . Proving the correctness of multiprocess programs . IEEE Trans. Softw. Eng. SE-3, 2 (Mar.) , 125 - 143 . LAMPORT, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2 (Mar.), 125-143.
LE~SENR~NG , A. C. 1969. Mathematical Logic and Hilbert's e-Symbol. Gordon and Breach , New York . LE~SENR~NG, A. C. 1969. Mathematical Logic and Hilbert's e-Symbol. Gordon and Breach, New York.
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 . 10.1145/41840.41852 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. 10.1145/41840.41852
MANNA , Z. AND PNUELI , A. 1991. The Temporal Logzc of Reactwe and Concurrent Systems . Springer-Vertag , New York . MANNA, Z. AND PNUELI, A. 1991. The Temporal Logzc of Reactwe and Concurrent Systems. Springer-Vertag, New York.
OWICKI , S. 1975. Axiomatic proof techniques for parallel programs. Ph. D. thesis , Cornell University , Ithaca N. Y. OWICKI, S. 1975. Axiomatic proof techniques for parallel programs. Ph. D. thesis, Cornell University, Ithaca N. Y.
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. 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.
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 . 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.
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. 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.
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. 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.