A. Udaya Shankar
Skip Abstract Section
Abstract
This is a tutorial introduction to assertional reasoning based on temporal logic. The objective is to provide a working familiarity with the technique. We use a simple system model and a simple proof system, and we keep to a minimum the treatment of issues such as soundness, completeness, compositionality, and abstraction. We model a concurrent system by a state transition system and fairness requirements. We reason about such systems using Hoare logic and a subset of linear-time temporal logic, specifically, invariant assertions and leads-to assertions. We apply the method to several examples.
- ABADI, M., AND LAIVIPORT, L. 1990. Composing specifications. In Stepwzse Refinement at' Distributed Systems. Lecture Notes m Computer Scmnce, vol 430, Sprmger-Verlag, New York. Also in ACM Trans. Program. Lang. Syst. 15, 1 (Jan 1993), 73-132.]] Google Scholar
- ABADI, M, AND LAMPORT, L. 1988. The existence of refinement mappings Tech. Rep. Dig4ta} Systems Research Center, Palo Alto, Calif Also in Theor Complit Scl 82, 2 (May 1991), 253 284.]] Google Scholar
- ALAI,}TTINOGLU, C., ANI/ SHANKaI~, A. U 1992 Stepwise assertional design of distance-vector routing algorithms In IFIP Proceedings o/the 12 International ~vmposzum on Protocol Specification, Testing, and Verification (Orlando, Fla, June). IFIP, Arhngton, Va.]] Google Scholar
- ALPERN, B., AND SCHNEIDER, F 1985. Defining liveness Inf. Process. Lett. 21, 4 (Oct.), 181 185]]Google Scholar
- ANDREWS, G. R 1989. A method for solving synchronization problems. Scl Comput. Program 13, 4 (Dee.), 1 21.]] Google Scholar
- APT, K. R. 1981. Ten years of Hoare's logm A survey--Part h ACM Trans Program Lang. Syst 3,4(Oct)431 483]] Google Scholar
- APT, K. R., FRANCEZ, N., AND }~4TZ, S. 1988. Apprmsing fairness in languages for distributed programming. Dzstrzb. Cornput. 2, 4, 226 241.]]Google Scholar
- BACK, R J R, AND KURKI-SuoNI(), R. 1988 Distributed cooperation with action system~. ACM Trans Program. Lang. Syst 10, 4 (Oct.), 513 554.]] Google Scholar
- BACK, R J. R., KU~KI-SUoNIO, R. 1983. Decentrahzation of process nets with a centralized control. In the 2nd ACM SIGACT-SIGCOPS Sympostzttn oil the Principles o/ Distributed Computilig (Montreal, Aug.) ACM, New York, 131 142.]] Google Scholar
- BACK, R. J. R., AND SERE, K. 1990. Stepw~se refinement of parallel algorithms Scl. Comput. Program. 13, 2-3, 133-180.]] Google Scholar
- CHaNDY, K. M. AND M/SRA, d 1998. A F~unrtotion of Parallel Program De.sign Addison-Wesley, Reading, Mass]] Google Scholar
- CHANI)Y, K. M., AND MISRA, J. 1986. An example of stepwlse refinement of distributed programs: Qmescence detectmn ACM Trans. Program. Lang. Syst. 8, 3 (July), 326-343.]] Google Scholar
- DI,IKSTRA, E W 1977 A correctness proof for communicating processes A small exermse. EWD-607, Burroughs, Nuenen, The Netherlands]]Google Scholar
- Dt.JKSTI~A, E.W. 1976 A Discipline of ProgrammlTlg Prentme-Hall, Englewood Cliffs, N.J.]]Google Scholar
- DI,JKSTRA, E.W. 1965 Solution of a problem in concurrent programming control. Cotnnlun. ACM 8, 9 (Sept)]] Google Scholar
- DI,JK~TI~A, E. W., AND SCHOLTEN, C.S. 1980. Termination detection for diffusing computations. Inf. Process. Lett 11 (Aug.), 1-4.]]Google Scholar
- DI,IKSTRA, E W., FEIJN, W. H. J., AND VAN GASTEREN, A. J. M. 1983. Derivation of a termination detection algorithm for distributed computations. Inf. Process. Lett. 16, 217 219.]]Google Scholar
- DI,JKSTRA, E. W., LAMPORT, L., MARTIN, A. J., AND SCItOLTEN, C. S. 1978. On-the-fly garbage collection: An exercise in cooperation Commun. ACM 21, 11 (Nov.), 966-975.]] Google Scholar
- DROST, N. J, AND SCHOONE, A.A. 1988. Asserhonal verification of a reset algorithm. R1jksuniverslteit Utrecht, RUU-CS-88-5.]]Google Scholar
- DROST, N. J., AND VAN LEEUWEN, J. 1988. Assertional verification of a majority consensus algorithm tbr concurrency control in multiple copy databases. Rijksuniversiteit Utrecht, RUU-CS- 88-13.]] Google Scholar
- FLoY/), R. W. 1967. Assigning' meanings to programs. In Proceedings o{ the Synzposzum on Applied Mothematzcs. Vol. 19. American Mathematical Society, 19 32,]]Google Scholar
- FI~ANCEZ, N. 1986. Fairness. Springer-Verlag, New York.]] Google Scholar
- GRIES, D 1981. The Sczence of Programming. Sprmger-Verlag, New York]] Google Scholar
- HAmPFRN, B. T., AN1) OWICKL S. S. 1983. Modular verification of computer communication protocols. IEEE Trans. Commun. COM-31, 1 (Jan.), 56 68.]]Google Scholar
- HOARE, C. A. R. 1985. Communicating Sequenhal Processes. Prentice-Hall, Englewood Cliffs, N.J.]] Google Scholar
- HOARE, C A. R. 1969. An axiomatic basra for computer programming. Commun. ACM 12, 10 (Oct.), 576-583.]] Google Scholar
- KNUTH, D.E. 1981. Vemfication of link-level protocols BIT21, 31 36.]]Google Scholar
- LAM, S. S., ANB SHANKAR, A.U. 1992 Specifying modules to satisfy interfaces: A state transition system approach. Dlstrlb. Comput. 6, 1, 39-63.]] Google Scholar
- LAM, S. S., ^N~) SHANKaR, A. U. 1990 A relational notation for state transition systems. IEEE Trans. Softw. Eng. 16 {July), 755 775.]] Google Scholar
- LAMPOm', L. 1991. The temporal logic of actions. DEC SRC Rep..57, Pale Alto, Calif' Revised 1991]]Google Scholar
- L^M,Om', L. 1990. A theorem on atomicity in distnbuted algorithms. Dzstnb. Comput. 4, 2, 59-68.]]Google Scholar
- LAMPORT, L. 1989. A simple approach to specifymg concurrent system~ Commun. AC3I 32, 1 (Jan.), 32-45.]] Google Scholar
- LAMPORT, L. 1987. A fast mutual exclusion algorithm. ACM Trans. Comput, Syst. 5, 1 (Feb), 1 11]] Google Scholar
- LAMPORT, L. 1983a. What good is temporal logic. in Proceedings of In/brmation Processing 83. IFIP, Arlington, Va.]]Google Scholar
- LAMPORT, L. 1983b. Specifying concurrent program modules. ACM Trans. Program. Lang. Syst. 5, 2 (Apr.), 190-222.]] Google Scholar
- LAMPORT, L. 1982. An assertional correctness proof of a distributed algorithm. Sez Comput. Program. 2, 3, 175-206.]]Google Scholar
- LAMPORT, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2 (Feb.), 125-143.]]Google Scholar
- LEHMAN, D., PNUELI, A., STAVI, J. 1981. hnpartiahty, justice, and fairness: The ethics of concurrent termination. In Proceedings of the 8th ICALP (Acre, Israel, July). Lecture Notes in Computer Science, vol. 115 Springer-Verlag, New York,]] Google Scholar
- LYNCH, N. A., AND TUTTLE, M.R. 1987. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the ACM Symposzunz on Prtnclples of Distributed Coraputmg (Vancouver, B C.). ACM, New York.]] Google Scholar
- MANNA, Z., AND PNUELI, A. 1984. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of' Computer Prog'rammmg, 4, 257-289.]] Google Scholar
- MANNA, Z., ANI~ PNUELL A. 1992. The Temporal Logw of Reactive and Concurrent Sv,stems: Speclfteatzon, Springer-Verlag, New York, 1992.]] Google Scholar
- MILNER, R. 1989. Comnzunzcotmn and Concurrency. Prentice-Hall, Englewood Cliffs, N.J]]Google Scholar
- MURPHY, S. L., AND SHANKAR, A. U. 1991 Connection management for the transport layer: Service specification and protocol construction. IEEE Trans. Commun. 39 (Dec.), 1762-1775.]]Google Scholar
- OWICKI, S., AND GRIES, D. 1976. An axiomatic proof technique for parallel programs I. Aeta In/brmatwa 6, 4, 319-340.]]Google Scholar
- OWICKI, S., AND LAMPORT, L. 1982. Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4 (July), 455 495.]] Google Scholar
- PETERSON, G.L. 1981. Myths about the mutual exclusion problem. Inf. Process. Lett. 12, 3 (June) 1133 1145]]Google Scholar
- PNUELI, A. 1984. In transition from global to modular temporal reasoning about programs. In NATO ASI Serzes, Logzcs and Models of Concurrent Systems. vol. F13. Springer-Verlag, Berlin, 123-144.]] Google Scholar
- PNUELI, A. 1979. The temporal semantics of concurrent programs. In Semantics of Concurrent Computation Lecture Notes in Computer Science, vol. 70. Springer-Verlag, New York, 1-20.]] Google Scholar
- PNEUM, A. 1977 The temporal logic of programs. In Proceedings o{ the 18th ACM Symposn~m on the Foundatmna' of Computer Seienoe. ACM, New York, 46 57.]]Google Scholar
- SCHNEmER, F. B., AND ANDREWS, G. R. 1986. Concepts for concurrent programming. In Current Trends m Concurrency. Lecture Notes in Computer Science, vol. 224. Springer-Verlag, New York, 669-716.]] Google Scholar
- SCHOONE, A A. 1987. Verification of connectionmanagement protocols. Rijksuniverslteit Utrecht, RUU-CS-87-14]]Google Scholar
- SHANKAR, A.U. 1989. Verified data transfer protocols with variable flow control. ACM Trans Comput. Syst. 7, 3 (Aug.), 281-316.]] Google Scholar
- SHANKAn, A. U., AND LAM, S S. 1992 A stepwise refinement heunstm for protocol construction. ACM Trans. Program Lang Syst 14, 3 (July), 417 461]] Google Scholar
- SHAN}OkR, A. U., AND LAM, S. S. 1987 Tramdependent distributed systems Proving safety, liveness and real-time propertms D~strlb. Comput. 2, 2, 61 79.]]Google Scholar
- SHANKAR, A. U, AND LAM, S.S. 1983 An HDLC protocol spemficatlon and its verification using image protocols. ACM Trans. Comput. Syst 1, 4 (Nov.), 331 368,]] Google Scholar
- SrSTLA, A. P. 1984 Distributed algorithms for ensuring fair lnterprocess communications In Proceedings of the ACM Symposium on Principles of Dlstrzbuted Cornpuhng (Vancouver, B.C, Aug.). ACM, New York.]] Google Scholar
- TEL, G 1987 Assertional verification of a timer-based protocol. R1jksunlversltmt Utrecht, RUU-CS-87-15.]]Google Scholar
- TEl., Cx., TAN, R B, AND VAN LEEUWEN, J. 1988 The derivation of' graph marking algomthms from distributed termmatmn detection protocols. Sci Comput. Program. 10, 2, 107-137.]] Google Scholar
Index Terms
- An introduction to assertional reasoning for concurrent systems
Recommendations
A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer ScienceMonads are the basis of a well-established method of encapsulating side-effects in semantics and programming. There have been a number of proposals for monadic program logics in the setting of plain monads, while much of the recent work on monadic ...
Inductive Completeness of Logics of Programs
We propose a new approach to delineating logics of programs, based directly on inductive definition of program semantics. The ingredients are elementary and well-known, but their fusion yields a simple yet powerful approach, surprisingly overlooked for ...
Substructural logic and partial correctness
We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and ...
Comments