
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Boutheina Chetali, "Formal Verification of Concurrent Programs Using the Larch Prover," IEEE Transactions on Software Engineering, vol. 24, no. 1, pp. 4662, January, 1998.  
BibTex  x  
@article{ 10.1109/32.663997, author = {Boutheina Chetali}, title = {Formal Verification of Concurrent Programs Using the Larch Prover}, journal ={IEEE Transactions on Software Engineering}, volume = {24}, number = {1}, issn = {00985589}, year = {1998}, pages = {4662}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.663997}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Formal Verification of Concurrent Programs Using the Larch Prover IS  1 SN  00985589 SP46 EP62 EPD  4662 A1  Boutheina Chetali, PY  1998 KW  Formal verification KW  protocol verification KW  communication protocol KW  theorem prover methodology KW  Larch prover KW  UNITY KW  computerchecked proof. VL  24 JA  IEEE Transactions on Software Engineering ER   
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 generalpurpose firstorder 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 computerchecked proof, and we show that a theorem prover can be used to detect flaws in a system specification.
[1] K. Chandy and J. Misra, Parallel Program Design: A Foundation. ISBN 0201058669. AddisonWesley, 1988.
[2] J. Guttag, J. Horning, S. Garland, K. Jones, A. Modet, and J. Wing, Larch: Languages and Tools for Formal Specification. SpringerVerlag, 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. 6985. SpringerVerlag, 1997.
[6] L. Lamport, "Proving the Correctness of Multiprocess Programs," IEEE Trans. Software Eng., vol. 3, no. 2, pp. 125143, 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. 349364. SpringerVerlag, 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. 227245. SpringerVerlag, 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. 185199. SpringerVerlag, 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. A5, NorthHolland, 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. 5568. SpringerVerlag, 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. 104141. SpringerVerlag, July 1992.
[16] J. SøgaardAnderson, S. Garland, J. Guttag, N. Lynch, and A. Pogosyants, "ComputedAssisted Simulation Proofs," Proc. Fifth Conf. ComputerAided Verification, C. Courcoubetis, ed., Lecture Notes in Computer Science 697, pp. 305319. SpringerVerlag, 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 0521441897. Cambridge Univ. Press, 1993.
[20] S. Owre, J. Rushby, N. Shankar, and F. von Henke, "Formal Verification for FaultTolerant Architectures: Prolegomena to the Design of PVS," IEEE Trans. Software Eng., vol. 21, pp. 107125, Feb. 1995.
[21] E. Dijkstra and C. Scholten, Predicate Calculus and Program Semantics. SpringerVerlag, 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 BoyerMoore Prover," IEEE Trans. Software Eng., vol. 16, pp. 1,0051,022, Sept. 1990.
[24] B. Chetali, "Proving Progress Properties Using the Larch Prover," Research Report 97R004, 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. 189205, 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 AlwaysTrue is not an Invariant," Information Processing Letters, vol. 40, pp. 231233, 1991.
[28] J. Pettersson, "Assertional Reasoning About Invariance," Research Report TFLRR19923, 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. 455495, July 1982.
[30] A. Borjesson, K. Larsen, and A. Skou, "Generality in Design and Compositional Verification Using TAV," IFIP Trans. C10: Formal Descriptions Techniques, pp. 449464, 1993.
[31] F. Andersen, "A Theorem Prover for Unity in HigherOrder Logic," PhD thesis, Technical Univ. of Denmark, 1992.
[32] B. Chetali, "Formal Verification of a LiftControl program Using the Larch Prover," Research Report 95R396, 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. 872923, 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. SpringerVerlag, 1991.