Formal Verification of Concurrent Programs Using the Larch Prover
|
Abstract—This paper describes the use of the Larch prover to verify concurrent programs. The chosen specification environment is UNITY, whose proposed model can be fruitfully applied to a wide variety of problems and modified or extended for special purposes. Moreover, UNITY provides a high level of abstraction to express solutions to parallel programming problems. We investigate how the UNITY methodology can be mechanized within a general-purpose first-order logic theorem prover like LP, and how we can use the theorem proving methodology to prove safety and liveness properties. Then we describe the formalization and the verification of a communication protocol over faulty channels, using the Larch prover LP. We present the full computer-checked proof, and we show that a theorem prover can be used to detect flaws in a system specification.
[1] 46 K. Chandy and J. Misra, Parallel Program Design: A Foundation. ISBN 0-201-05866-9. Addison-Wesley, 1988.
[2] J. Guttag, J. Horning, S. Garland, K. Jones, A. Modet, and J. Wing, Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
[3] S. Garland and J. Guttag, "A Guide to LP, the Larch Prover," Technical Report 82, Digital Systems Research Center, Palo Alto, Calif., 1991.
[4] E.W. Dijkstra, A Discipline of Programming.Englewood Cliffs, N.J.: Prentice Hall, 1976.
[5] B. Chetali and B. Heyd, "Formal Verification in LP and in Coq: A Comparative Analysis," Proc. 10th Int'l Conf. Theorem Proving in Higher Order Logics, E.Gunter and A. Felty, eds., Lecture Notes in Computer Science 275, pp. 69-85. Springer-Verlag, 1997.
[6] L. Lamport, "Proving the Correctness of Multiprocess Programs," IEEE Trans. Software Eng., vol. 3, no. 2, pp. 125-143, 1977.
[7] J. Misra, "A Logic for Concurrent Programming," 1994, unpublished manuscripts.
[8] S. Garland, J.V. Guttag, and J. Staunstrup, "Verification of VLSI Circuits Using LP," Proc. IFIP WG 10.2, The Fusion of Hardware Design and Verification,B.V. North Holland: Elsevier Science, 1988.
[9] J.V. Staunstrup, S. Garland, and J.V. Guttag, "Localized Verification of Circuit Descriptions," Proc. Workshop Automatic Verification Methods for Finite State Systems, J. Sifakis, ed., Lecture Notes in Computer Science 407, pp. 349-364. Springer-Verlag, 1989.
[10] E. Scott and K. Norrie, "Using LP to Study the Language PL," Proc. First Int'l Workshop on Larch, U. Martin and J.M. Wing, eds., Workshops in Computing 780, pp. 227-245. Springer-Verlag, July 1992.
[11] N. Mellergaard and J. Staunstrup, "Generating Proof Obligations for Circuits," Proc. First Int'l Workshop on Larch, U. Martin and J.M. Wing, eds., Workshops in Computing 780, pp. 185-199. Springer-Verlag, July 1992.
[12] J. Saxe, S. Garland, J. Guttag, and J. Horning, "Using Transformations and Verification in Circuit Design," Proc. Int'l Workshop Designing Correct Circuits, J. Staunstrup and R. Sharp, eds., IFIP Trans. A-5, North-Holland, 1992.
[13] B. Chetali and P. Lescanne, "An Exercise in LP: The Proof of the Non Restoring Division Circuit," Proc. First Int'l Workshop on Larch, U. Martin and J.M. Wing, eds., Workshops in Computing 780, pp. 55-68. Springer-Verlag, July 1992.
[14] M. Allemand, "Modélisation fonctionnelle et preuves de circuits avec LP [Functional Modeling and Hardware Verification Using LP]," PhD thesis, Universitéde Provence, France, 1995.
[15] D. Guaspari, C. Marceau, and W. Polak, "Formal Verification of ADA Programs," Proc. First Int'l Workshop on Larch, U. Martin and J.M. Wing, eds., Workshops in Computing 780, pp. 104-141. Springer-Verlag, July 1992.
[16] J. Søgaard-Anderson, S. Garland, J. Guttag, N. Lynch, and A. Pogosyants, "Computed-Assisted Simulation Proofs," Proc. Fifth Conf. Computer-Aided Verification, C. Courcoubetis, ed., Lecture Notes in Computer Science 697, pp. 305-319. Springer-Verlag, 1993.
[17] D. Doligez and G. Gonthier, "Portable, Unobtrusive Garbage Collection for Multiprocessor Systems," Proc. POPL'94, ACM, 1994.
[18] V. Luchangco, E. Söylemez, S. Garland, and N. Lynch, "Verifying Timing Properties of Concurrent Algorithms," Proc. Seventh Int'l Conf. Formal Description Techniques,Berne, Switzerland: Chapman and Hall, Oct. 1994.
[19] M.-J.-C. Gordon and T.-F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. ISBN 0-521-44189-7. Cambridge Univ. Press, 1993.
[20] S. Owre, J. Rushby, N. Shankar, and F. von Henke, "Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS," IEEE Trans. Software Eng., vol. 21, pp. 107-125, Feb. 1995.
[21] E. Dijkstra and C. Scholten, Predicate Calculus and Program Semantics. Springer-Verlag, 1989.
[22] B. Chetali, Vérification Formelle des Systémes Paralléles décrits en UNITYál'aide d'un outil de Démonstration Automatique "Formal Verification of Concurrents Systems described in Unity, Using a Theorem Prover," PhD thesis, Henri PoincaréUniv. of Nancy I, France, May 1996.
[23] D. Goldschlag, "Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover," IEEE Trans. Software Eng., vol. 16, pp. 1,005-1,022, Sept. 1990.
[24] B. Chetali, "Proving Progress Properties Using the Larch Prover," Research Report 97-R-004, Centre Recherche en Informatique de Nancy, CRIN, France, 1997.
[25] B. Sanders, "Eliminating the Substitution Axiom from Unity Logic," Formal Aspects of Computing, vol. 3, pp. 189-205, 1991.
[26] B. Chetali and P. Lescanne, "Formal Verification of a Protocol for Communications Over Faulty Channels," Proc. Eighth Int'l Conf. Formal Description Techniques for Distributed Systems and Communications Protocols,Montréal, Quebec, Canada, IFIP. Chapman and Hall, Oct. 1995.
[27] J. Pettersson, "Comments on Always-True is not an Invariant," Information Processing Letters, vol. 40, pp. 231-233, 1991.
[28] J. Pettersson, "Assertional Reasoning About Invariance," Research Report TFL-RR-1992-3, Tele Denmark Research, June 1992.
[29] L. Lamport and S. Owicki, "Proving Liveness Properties of Concurrent Programs," ACM Trans. Programming Languages and Systems, vol. 4, pp. 455-495, July 1982.
[30] A. Borjesson, K. Larsen, and A. Skou, "Generality in Design and Compositional Verification Using TAV," IFIP Trans. C-10: Formal Descriptions Techniques, pp. 449-464, 1993.
[31] F. Andersen, "A Theorem Prover for Unity in Higher-Order Logic," PhD thesis, Technical Univ. of Denmark, 1992.
[32] B. Chetali, "Formal Verification of a Lift-Control program Using the Larch Prover," Research Report 95-R-396, Centre de Recherche en Informatique de Nancy, CRIN, France, 1995.
[33] L. Lamport and S. Owicki, "The Temporal Logic of Actions," ACM Trans. Programming Languages and Systems, vol. 16, pp. 872-923, May 994.
[34] U.H. Engberg, "Reasoning in the Temporal Logic of Actions," PhD thesis, Aarhus Univ., Denmark, 1995.
[35] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
Index Terms:
Formal verification, protocol verification, communication protocol, theorem prover methodology, Larch prover, UNITY, computer-checked proof.
Citation:
Boutheina Chetali, "Formal Verification of Concurrent Programs Using the Larch Prover," IEEE Transactions on Software Engineering, vol. 24, no. 1, pp. 46-62, Jan. 1998, doi:10.1109/32.663997
PURCHASE ARTICLE: $19
IEEE Xplore Subscribers
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb