Advertisement

Formal Methods

  • Doron A. Peled
Chapter
First Online:

Abstract

Formal methods is a collection of techniques for improving the reliability of systems, based on mathematics and logics. While testing is still the most commonly used method for debugging and certifying software systems, newer techniques such as program verification and model checking are already in common use by major software houses. Tools for supporting these techniques are constantly being developed and improved, both in industry and in academia. This multidisciplinary research and development area gains a lot of attention, due to the rapidly growing number of critical roles that computer systems play. This chapter describes some of the main formal techniques, while presenting their advantages and limitations.

This is a preview of subscription content, log in to check access.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aggarwal, S., Kurshan, R.P., Sabnani, K.K.: A calculus for protocol specification and validation. In: Protocol Specification, Testing, and Verification, pp. 19–34 (1983)Google Scholar
  2. 2.
    Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)zbMATHCrossRefGoogle Scholar
  3. 3.
    Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Proceedings of ICALP, pp. 322–335 (1990)Google Scholar
  4. 4.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  5. 5.
    Alur, R., Holzmann, G.J., Peled, D.A.: An analyzer for message sequence charts. Softw. Concepts Tools 17(2), 70–77 (1996)Google Scholar
  6. 6.
    Alur, R., McMillan, K.L., Peled, D.A.: Deciding global partial-order properties. In: Proceedings of ICALP, pp. 41–52 (1998)CrossRefGoogle Scholar
  7. 7.
    Apt, K.R.: Ten years of Hoare’s logic: a survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)zbMATHCrossRefGoogle Scholar
  8. 8.
    Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Automated verification of quantum protocols by equivalence checking. In: Proceedings of TACAS, pp. 500–514 (2014)Google Scholar
  10. 10.
    Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M.Z., Ryan, M.: Symbolic model checking for probabilistic processes. In: Proceedings of ICALP, pp. 430–440 (1997)CrossRefGoogle Scholar
  11. 11.
    Basin, D.A., Klaedtke, F., Marinovic, S., Zalinescu, E.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des. 46(3), 262–285 (2015)zbMATHCrossRefGoogle Scholar
  12. 12.
    Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Proceedings of Hybrid Systems, pp. 232–243 (1995)CrossRefGoogle Scholar
  13. 13.
    Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Proceedings of CAV, pp. 319–331 (1998)CrossRefGoogle Scholar
  14. 14.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Proceedings of CONCUR, pp. 135–150 (1997)CrossRefGoogle Scholar
  15. 15.
    Boyer, R.S., Moore, J.S.: Computational Logic. Academic, New York (1979)zbMATHGoogle Scholar
  16. 16.
    Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  17. 17.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. Z. Math. Logik Grundlag. Math 6, 66–92 (1960)zbMATHCrossRefGoogle Scholar
  18. 18.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proceedings of LICS, pp. 428–439 (1990)Google Scholar
  19. 19.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, pp. 52–71 (1981)Google Scholar
  20. 20.
    Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7–34 (2001)zbMATHCrossRefGoogle Scholar
  21. 21.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  22. 22.
    Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proceedings of FOCS, pp. 338–345 (1988)Google Scholar
  23. 23.
    Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods Syst. Des. 1, 275–288 (1992)zbMATHCrossRefGoogle Scholar
  24. 24.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL, pp. 238–252 (1977)Google Scholar
  25. 25.
    de Moura, L.Me., Bjorner, N.: Z3, an efficient SMT solver. In: Proceedings of TACAS, pp. 337–340 (2008)Google Scholar
  26. 26.
    Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965)CrossRefGoogle Scholar
  27. 27.
    Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated Circuits and Systems. Springer, Berlin (2006)Google Scholar
  28. 28.
    Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Proceedings of ICALP, pp. 169–181 (1980)CrossRefGoogle Scholar
  29. 29.
    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)MathSciNetzbMATHCrossRefGoogle Scholar
  30. 30.
    Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, pp. 19–32. American Mathematical Society, Providence (1967)Google Scholar
  31. 31.
    Francez, N.: Fairness, Texts and Monographs in Computer Science, pp. 1–295. Springer, Berlin (1986)zbMATHCrossRefGoogle Scholar
  32. 32.
    Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of PSTV, pp. 3–18 (1995)CrossRefGoogle Scholar
  33. 33.
    Godefroid, P., Wolper, P.: A partial approach to model checking. In: Proceedings of LICS, pp. 406–415 (1991)Google Scholar
  34. 34.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI, pp. 213–223 (2005)CrossRefGoogle Scholar
  35. 35.
    Gödel, K.: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. Monatsh. Math. Phys. 38(1), 173–198 (1931)MathSciNetzbMATHCrossRefGoogle Scholar
  36. 36.
    Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)zbMATHGoogle Scholar
  37. 37.
    Grosu, R., Smolka, S.A.: Monte Carlo model checking. In: Proceedings of TACAS, pp. 271–286 (2005)CrossRefGoogle Scholar
  38. 38.
    Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: Proceedings of Automated Software Engineering, November 2001, pp. 135–143 (2001)Google Scholar
  39. 39.
    Havelund, K., Peled, D.A., Ulus, D.: First order temporal logic monitoring with BDDs. In: Proceedings of FMCAD, pp. 116–123 (2017)Google Scholar
  40. 40.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)zbMATHCrossRefGoogle Scholar
  41. 41.
    Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)Google Scholar
  42. 42.
    Holzmann, G.J., Peled, D.A., Yannakakis, M.: On nested depth first search. In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 23–31 (1996)zbMATHGoogle Scholar
  43. 43.
    Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)CrossRefGoogle Scholar
  44. 44.
    Katz, G., Peled, D.A.: Synthesizing, correcting and improving code, using model checking-based genetic programming. Int. J. Softw. Tools Technol. Transfer 19(4), 449–464 (2017)CrossRefGoogle Scholar
  45. 45.
    Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on Common Lisp. IEEE Trans. Softw. Eng. 23, 203–213 (1997)CrossRefGoogle Scholar
  46. 46.
    Könighofer, B., Alshiekh, M., Bloem, R., Humphrey, L., Könighofer, R., Topcu, U., Wang, C.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332–361 (2017)zbMATHCrossRefGoogle Scholar
  47. 47.
    Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. EATCS Series, pp. 1–304. Springer, Berlin (2008)Google Scholar
  48. 48.
    Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Proceedings of CAV, pp. 172–183 (1999)CrossRefGoogle Scholar
  49. 49.
    Lamport, L.: “Sometimes” is sometimes “not never”. In: Proceedings of POPL, pp. 175–185 (1980)Google Scholar
  50. 50.
    Larsen, K.G., Peled, D.A., Sedwards, S.: Memory-efficient tactics for randomized LTL model checking. In: Proceedings of VSTTE, pp. 152–169 (2017)Google Scholar
  51. 51.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Proceedings of RV, pp. 122–135 (2010)CrossRefGoogle Scholar
  52. 52.
    Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language. In: Proceedings of POPL, pp. 141–154 (1983)Google Scholar
  53. 53.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, Berlin (1991)Google Scholar
  54. 54.
    Mazurkiewicz, A.W.: Trace theory. In: Proceedings of Advances in Petri Nets, pp. 279–324 (1986)Google Scholar
  55. 55.
    McConnel, S.: Code Complete - A Practical Handbook of Software Construction, 2nd edn. Microsoft Press, Redmond (2004)Google Scholar
  56. 56.
    McMillan, K.L.: Interpolation and SAT-based model checking. In: Proceedings of CAV, pp. 1–13 (2003)Google Scholar
  57. 57.
    McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in compositional model checking. In: Proceedings of CAV, pp. 312–327 (2000)CrossRefGoogle Scholar
  58. 58.
    Meyers, G.J.: The Art of Software Testing. Wiley, Hoboken (1979). 1989, ISBN 978-0-13-115007-2, pp. I-XI, 1–260Google Scholar
  59. 59.
    Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)Google Scholar
  60. 60.
    O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of CSL, pp. 1–19 (2001)Google Scholar
  61. 61.
    Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatic 6, 319–340 (1976)MathSciNetzbMATHCrossRefGoogle Scholar
  62. 62.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Proceedings of CADE, pp. 748–752 (1992)CrossRefGoogle Scholar
  63. 63.
    Peled, D.A.: All from one, one for all, on model checking using representatives. In: Proceedings of CAV, pp. 409–423 (1993)CrossRefGoogle Scholar
  64. 64.
    Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46–57 (1977)Google Scholar
  65. 65.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of POPL, pp. 179–190 (1989)Google Scholar
  66. 66.
    Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of FOCS, pp. 746–757 (1990)Google Scholar
  67. 67.
    Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. Symposium on Programming, pp. 337–351 (1982)Google Scholar
  68. 68.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS, pp. 55–74 (2002)Google Scholar
  69. 69.
    Ryan, P.Y.A., Schneider, S.A.: Modelling and Analysis of Security Protocols, pp. 1–300. Addison-Wesley-Longman, Boston (2001)Google Scholar
  70. 70.
    Safra, S.: On the complexity of omega-automata. In: Proceedings of FOCS, pp. 319–327 (1988)Google Scholar
  71. 71.
    Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997)CrossRefGoogle Scholar
  72. 72.
    Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Proceedings of CAV, pp. 419–423 (2006)Google Scholar
  73. 73.
    Solar-Lezama, A., Rabbah, R.M., Bodik, R., Ebciogl, K.: Programming by sketching for bit-streaming programs. In: Proceedings of PLDI, pp. 281–294 (2005)CrossRefGoogle Scholar
  74. 74.
    Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pp. 133–192. MIT Press, Cambridge (1990)Google Scholar
  75. 75.
    Valmari, A.: Stubborn sets for reduced state space generation. In: Proceedings of Applications and Theory of Petri Nets, pp. 491–515 (1989)CrossRefGoogle Scholar
  76. 76.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (Preliminary Report). In: Proceedings of LICS, pp. 332–344 (1986)Google Scholar
  77. 77.
    Walukiewicz, I.: Difficult configurations - on the complexity of LTrL. In: Proceedings of ICALP, pp. 140–151 (1998)CrossRefGoogle Scholar
  78. 78.
    Winskel, G.: Event structures. In: Proceedings of Advances in Petri Nets, pp. 325–392 (1986)CrossRefGoogle Scholar
  79. 79.
    Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Proceedings of CAV, pp. 223–235 (2002)zbMATHCrossRefGoogle Scholar
  80. 80.
    Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1–2), 135–183 (1998)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Doron A. Peled
    • 1
  1. 1.Bar Ilan UniversityRamat GanIsrael

Personalised recommendations

Cite chapter

Buy options