Advertisement

An Overview of Formal Methods Tools and Techniques

  • José Bacelar Almeida
  • Maria João Frade
  • Jorge Sousa Pinto
  • Simão Melo de Sousa
Part of the Undergraduate Topics in Computer Science book series (UTICS)

Abstract

The goal of this chapter is to give an overview of the different approaches and tools pertaining to formal methods. We do not attempt to be exhaustive, but focus instead on the main approaches (formal specification, formal verification and proofs, transformation, and formal development). A consise introduction to basic logic concepts and methods is also provided. After reading the chapter the reader will be familiar with the terminology of the area, as well as with the most important concepts and techniques.

Moreover the chapter will allow the reader to contextualise and put into perspective the topics that are covered in detail in the book.

Keywords

Programming Language Model Check Formal Method Formal Verification Proof Obligation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Abdulla, P.A., Deneux, J.: Designing safe, reliable systems using scade. In: Proc. ISoLA 2004 (2004) Google Scholar
  2. 2.
    Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996) MATHCrossRefGoogle Scholar
  3. 3.
    Abrial, J.-R.: Modeling in Event-B System and Software Engineering. Cambridge University Press, Cambridge (2010) MATHCrossRefGoogle Scholar
  4. 4.
    Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Softw. Syst. Model.4, 32–54 (2005) CrossRefGoogle Scholar
  5. 5.
    Alur, R., Dill, D.: Automata-theoretic verification of real-time systems. In: Formal Methods for RealTime Computing. Trends in Software Series, pp. 55–82. Wiley, New York (1996) Google Scholar
  6. 6.
    Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci.126(2), 183–235 (1994) MathSciNetMATHCrossRefGoogle Scholar
  7. 7.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci.126(2), 183–235 (1994) MathSciNetMATHCrossRefGoogle Scholar
  8. 8.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) Google Scholar
  9. 9.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008) MATHGoogle Scholar
  10. 10.
    Barendregt, H.P.: The Lambda Calculus, its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1984) MATHGoogle Scholar
  11. 11.
    Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 117–310. Oxford University Press, New York (1992) Google Scholar
  12. 12.
    Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, vol. 3362, pp. 49–69. Springer, Berlin (2004) CrossRefGoogle Scholar
  13. 13.
    Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Proceedings of the 19th International Conference on Computer Aided Verification (CAV ’07). Lecture Notes in Computer Science, vol. 4590, pp. 298–302. Springer, Berlin (2007) CrossRefGoogle Scholar
  14. 14.
    Barthe, G., Courtieu, P., Dufay, G., de Sousa, S.M.: Tool-assisted specification and verification of typed low-level languages. J. Autom. Reason.35(4), 295–354 (2005) MATHCrossRefGoogle Scholar
  15. 15.
    Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: Shao, Z., Pierce, B.C. (eds.) POPL, pp. 90–101. ACM, New York (2009) Google Scholar
  16. 16.
    Baudin, P., Fillitre, J.-C., March, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. Preliminary Design (version 1.4). From the Frama-C website,http://frama-c.com (2010)
  17. 17.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial onuppaal. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Berlin (2004) Google Scholar
  18. 18.
    Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages 12 years later. Proc. IEEE91(1), 64–83 (2003) CrossRefGoogle Scholar
  19. 19.
    Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification. Model-Checking Techniques and Tools. Springer, Berlin (2001) MATHCrossRefGoogle Scholar
  20. 20.
    van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) Proceedings of TACAS’01. Lecture Notes in Computer Science, vol. 2031, pp. 299–312. Springer, Berlin (2001) Google Scholar
  21. 21.
    Bezem, M., Klop, J.W., de Vrijer, R. (eds.): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2002) Google Scholar
  22. 22.
    Bidoit, M., Mosses, P.D.:Casl User Manual. LNCS (IFIP Series), vol. 2900. Springer, Berlin (2004). With chapters by T. Mossakowski, D. Sannella, and A. Tarlecki MATHCrossRefGoogle Scholar
  23. 23.
    Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. CoRR, abs/cs/0701193 (2007) Google Scholar
  24. 24.
    Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language Lotos. Comput. Netw. ISDN Syst.14(1), 25–59 (1987) CrossRefGoogle Scholar
  25. 25.
    Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E., Ringeissen, C.: An overview of ELAN. In: Kirchner, C., Kirchner, H. (eds.) Proceedings of the International Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 15. Pont-à-Mousson, France, September 1998. Elsevier, Amsterdam (1998) Google Scholar
  26. 26.
    Bouhoula, A., Kounalis, E., Rusinowitch, M.: SPIKE, an automatic theorem prover. In: Voronkov, A. (ed.) Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR’92). Lecture Notes in Artificial Intelligence, vol. 624, pp. 460–462. Springer, Berlin (1992) CrossRefGoogle Scholar
  27. 27.
    Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda—a functional language with dependent types. In: TPHOLs ’09: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, pp. 73–78. Springer, Berlin (2009) CrossRefGoogle Scholar
  28. 28.
    Bowen, J.P., Hinchey, M.G.: Seven more myths of formal methods. IEEE Softw.12(4), 34–41 (1995) CrossRefGoogle Scholar
  29. 29.
    Bowen, J.P., Hinchey, M.G.: Ten commandments of formal methods. Computer28(4), 56–63 (1995) CrossRefGoogle Scholar
  30. 30.
    Bowen, J.P., Hinchey, M.G.: Ten commandments of formal methods … ten years later. Computer39(1), 40–48 (2006) CrossRefGoogle Scholar
  31. 31.
    Bowen, J.P., Stavridou, V.: Safety-critical systems, formal methods and standards. IEE/BCS Softw. Eng. J.8(4), 189–209 (1993) CrossRefGoogle Scholar
  32. 32.
    Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems (1998) Google Scholar
  33. 33.
    Burstall, R.M., Goguen, J.A.: An informal introduction to specification using CLEAR. In: Boyer, R.S., Moore, J.S. (eds.) The Correctness Problem in Computer Science, pp. 185–213. Academic Press, New York (1981) Google Scholar
  34. 34.
    Carré, B., Garnsworthy, J.: Spark—an annotated Ada subset for safety-critical programming. In: TRI-Ada ’90: Proceedings of the Conference on TRI-ADA ’90, pp. 392–402. ACM, New York (1990) CrossRefGoogle Scholar
  35. 35.
    Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: A declarative language for real-time programming. In: POPL ’87: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 178–188. ACM, New York (1987) CrossRefGoogle Scholar
  36. 36.
    Clarke, E.M., Wing, M.J.: Formal methods: State of the art and future directions. ACM Comput. Surv.28(4), 626–643 (1996) CrossRefGoogle Scholar
  37. 37.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999) Google Scholar
  38. 38.
    Cockett, R., Fukushima, T.: About Charity. Technical Report 92/480/18, University of Calgary (June 1992) Google Scholar
  39. 39.
    CoFI (The Common Framework Initiative):Casl Reference Manual. LNCS (IFIP Series), vol. 2960. Springer, Berlin (2004) Google Scholar
  40. 40.
    Colin, S., Petit, D., Mariano, G., Poirriez, V.: BRILLANT: An open source platform for B. In: Workshop on Tool Building in Formal Methods (held in conjunction with ABZ2010), February 2010 Google Scholar
  41. 41.
    Colin, S., Petit, D., Poirriez, V., Rocheteau, J., Marcano, R., Mariano, G.: BRILLANT: An open source and XML-based platform for rigourous software development. In: SEFM ’05: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, Washington, DC, USA, 2005, pp. 373–382. IEEE Computer Society, Los Alamitos (2005) CrossRefGoogle Scholar
  42. 42.
    Conchon, S., Contejean, E., Kanig, J.: Ergo: A theorem prover for polymorphic first-order logic modulo theories (2006) Google Scholar
  43. 43.
    Correnson, L., Cuoq, P., Puccetti, A., Signoles, J.: Frama-C user manual. From the Frama-C website,http://frama-c.com (2010)
  44. 44.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, pp. 238–252. ACM, New York (1977) Google Scholar
  45. 45.
    Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contract-based modular verification of concurrent C Google Scholar
  46. 46.
    De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2008) Google Scholar
  47. 47.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. J. ACM52(3), 365–473 (2005) MathSciNetCrossRefGoogle Scholar
  48. 48.
    Dutertre, B., De Moura, L.: The Yices SMT solver. Technical report, SRI (2006) Google Scholar
  49. 49.
    Dwyer, M., Hatcliff, J., Joehanes, R., Laubach, S., Pasareanu, C., Visser, R.W., Zheng, H.: Tool-supported program abstraction for finite-state verification. In: Proceedings of ICSE’01 (2001) Google Scholar
  50. 50.
    Dybvig, R.K.: The Scheme Programming Language: ANSI Scheme, 2nd edn. Prentice-Hall International, Upper Saddle River (1996) Google Scholar
  51. 51.
    Ehrig, H., Fey, W., Hansen, H.: ACT ONE: An algebraic specification language with two levels of semantics. Technical Report 83–03, Technical University of Berlin, Fachbereich Informatik (1983) Google Scholar
  52. 52.
    Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: International Symposium on FME 2001: Formal Methods for Increasing Software Productivity. Lecture Notes in Computer Science, vol. 2021, pp. 500–517. Springer, Berlin (2001) CrossRefGoogle Scholar
  53. 53.
    Formal methods ressources.http://www.afm.sbu.ac.uk/
  54. 54.
    Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ-2. In: Reid, B. (ed.) Proceedings 12th ACM Symp. on Principles of Programming Languages, pp. 52–66. Association for Computing Machinery, New York (1985) Google Scholar
  55. 55.
    Garland, S.J., Guttag, J.V., Horning, J.: An Overview of Larch. Lecture Notes in Computer Science, vol. 693, pp. 329–348. Springer, Berlin (1993) Google Scholar
  56. 56.
    George, C., Haxthausen, A.E., Hughes, S., Milne, R., Prehn, S., Pedersen, J.S.: The Raise Development Method. Prentice-Hall International, London (1995) MATHGoogle Scholar
  57. 57.
    Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993) MATHGoogle Scholar
  58. 58.
    Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995) Google Scholar
  59. 59.
    Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer Academic, Norwell (1993) MATHGoogle Scholar
  60. 60.
    Hall, A.: Seven myths of formal methods. IEEE Softw.7(5), 11–19 (1990) CrossRefGoogle Scholar
  61. 61.
    Hartel, P.H., Moreau, L.: Formalizing the safety of Java, the Java virtual machine, and Java card. ACM Comput. Surv.33(4), 517–558 (2001) CrossRefGoogle Scholar
  62. 62.
    Henzinger, T.A.: The theory of hybrid automata. In: LICS ’96: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, 1996, p. 278. IEEE Computer Society, Los Alamitos (1996) CrossRefGoogle Scholar
  63. 63.
    Henzinger, T.A., Ho, P.-H., Wong-toi, H.: Hytech: A model checker for hybrid systems. Softw. Tools Technol. Transf.1, 460–463 (1997) Google Scholar
  64. 64.
    Hoare, C.A.R., Misra, J.: Preface to special issue on software verification. ACM Comput. Surv.41(4), 1–3 (2009) Google Scholar
  65. 65.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006) Google Scholar
  66. 66.
    JML Specification Language.http://www.jmlspecs.org
  67. 67.
    Jones, C.B.: Software Development. A Rigorous Approach. Prentice-Hall International, Englewood Cliffs (1980) MATHGoogle Scholar
  68. 68.
    Juellig, R., Srinivas, Y., Liu, J.: SPECWARE: An advanced environment for the formal development of complex software systems. In: Proceedings of AMAST’96. Lecture Notes in Computer Science, vol. 1101, pp. 551–554. Springer, Berlin (1996) Google Scholar
  69. 69.
    Kaufmann, M., Strother Moore, J.: ACL2: An industrial strength version of Nqthm. COMPASS—Proceedings of the Annual Conference on Computer Assurance, pp. 23–34 (1996). IEEE catalog number 96CH35960 Google Scholar
  70. 70.
    Klein, G.: Correct os kernel? proof? done! USENIX ;login:34(6), 28–34 (2009) Google Scholar
  71. 71.
    Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: sel4: Formal verification of an os kernel. In: Matthews, J.N., Anderson, T.E. (eds.) SOSP, pp. 207–220. ACM, New York (2009) CrossRefGoogle Scholar
  72. 72.
    Klop, J.W.: Term-rewriting systems. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 1–116. Oxford Science Publications, New York (1992) Google Scholar
  73. 73.
  74. 74.
    Krauss, K.G.: Petri Nets Applied to the Formal Verification of Parallel and Communicating Processes. Lehigh University, Dissertation, Bethlehem, PA (1987) Google Scholar
  75. 75.
    Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system, release 3.06 (2002).http://caml.inria.fr
  76. 76.
    Leroy, Xavier: Formal verification of a realistic compiler. Commun. ACM52(7), 107–115 (2009) CrossRefGoogle Scholar
  77. 77.
    Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. (STTT)10(2), 185–203 (2008) CrossRefGoogle Scholar
  78. 78.
    Mazzeo, A., Mazzocca, N., Russo, S., Savy, C., Vittorini, V.: Formal specification of concurrent systems: a structured approach. Comput. J.41(3), 145–162 (1998) MATHCrossRefGoogle Scholar
  79. 79.
    The Coq development team. The Coq proof assistant reference manual. LogiCal Project (2008). Version 8.2 Google Scholar
  80. 80.
    Meyer, B.: Eiffel: The Language. Prentice Hall, Hemel Hempstead (1992) MATHGoogle Scholar
  81. 81.
    Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997) Google Scholar
  82. 82.
    Monin, J.F.: Understanding Formal Methods. Springer, New York (2001) Google Scholar
  83. 83.
    Paulson, L.: Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 828. Springer, Berlin (1994) MATHGoogle Scholar
  84. 84.
    Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010) MATHCrossRefGoogle Scholar
  85. 85.
    Platzer, A., Quesel, J.-D.: KeYmaera: A hybrid theorem prover for hybrid systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR. LNCS, vol. 5195, pp. 171–178. Springer, Berlin (2008) Google Scholar
  86. 86.
    Reisig, W.: Petri nets and algebraic specifications. Theor. Comput. Sci.80, 1–34 (1991) MathSciNetMATHCrossRefGoogle Scholar
  87. 87.
    Requet, A.: An overview of Atelier B 4.0. In: Proceedings of the Conference The B Formal Method: From Research to Teaching’2008, Nantes (June 2008) Google Scholar
  88. 88.
    Rushby, J.: Formal methods and their role in the certification of critical systems. Technical Report SRI-CSL-95-1, Computer Science Laboratory, SRI International, Menlo Park, CA (March 1995) Google Scholar
  89. 89.
    Rushby, J.: Formal specification and verification for critical systems: Tools, achievements, and prospects. In: Suri, N., Walter, C.J., Hugue, M.M. (eds.) Advances in Ultra-Dependable Distributed Systems, pp. 282–296. IEEE Computer Society, Los Alamitos (1995) Google Scholar
  90. 90.
    Sannella, D.: A survey of formal software development methods. Technical Report ECS-LFCS-88-56, University of Edinburgh (July 1988) Google Scholar
  91. 91.
    Shankar, N., Owre, S., Rushby, J.M.: The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International (February 1993) Google Scholar
  92. 92.
    Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, vol. 149. Elsevier, Amsterdam (2006) Google Scholar
  93. 93.
    Spivey, J.: An introduction to Z and formal specification. IEEE Softw. Eng. J.4(1), 40–50 (1989) CrossRefGoogle Scholar
  94. 94.
    Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine—Definition, Verification, Validation. Springer, Berlin (2001) MATHCrossRefGoogle Scholar
  95. 95.
    Sterling, L., Shapiro, E.: The Art of Prolog, 2nd edn. MIT Press, Cambridge (1994) MATHGoogle Scholar
  96. 96.
    Thompson, S.: Haskell: The Craft of Functional Programming. Int. Comupt. Sci. Pearson Edn (1999) Google Scholar
  97. 97.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symposium on Logic in Computer Science (LICS’86), pp. 332–345. IEEE Computer Society Press, Los Alamitos (1986) Google Scholar
  98. 98.
    Verma, K.N., Goubault-Larrecq, J.: Reflecting BDDs in Coq. Technical Report RR3859, INRIA projet Coq (January 2000) Google Scholar
  99. 99.
    Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv.41(4), 1–36 (2009) CrossRefGoogle Scholar
  100. 100.
    Wu, W., Saeki, M.: Specifying software architectures based on colored petri nets. IEICE Trans. Inf. Syst.E83-D(4), 701–712 (2000) Google Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  • José Bacelar Almeida
    • 1
  • Maria João Frade
    • 2
  • Jorge Sousa Pinto
    • 1
  • Simão Melo de Sousa
    • 2
  1. 1.Depto. InformáticaUniversidade do MinhoBragaPortugal
  2. 2.Depto. InformáticaUniversidade Beira InteriorCovilhãPortugal

Personalised recommendations