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.
Preview
Unable to display preview. Download preview PDF.
References
- 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.Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)zbMATHCrossRefGoogle Scholar
- 3.Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Proceedings of ICALP, pp. 322–335 (1990)Google Scholar
- 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.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.Alur, R., McMillan, K.L., Peled, D.A.: Deciding global partial-order properties. In: Proceedings of ICALP, pp. 41–52 (1998)CrossRefGoogle Scholar
- 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.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.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.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.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.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.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.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.Boyer, R.S., Moore, J.S.: Computational Logic. Academic, New York (1979)zbMATHGoogle Scholar
- 16.Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
- 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.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.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.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.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.Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proceedings of FOCS, pp. 338–345 (1988)Google Scholar
- 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.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.de Moura, L.Me., Bjorner, N.: Z3, an efficient SMT solver. In: Proceedings of TACAS, pp. 337–340 (2008)Google Scholar
- 26.Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965)CrossRefGoogle Scholar
- 27.Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated Circuits and Systems. Springer, Berlin (2006)Google Scholar
- 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.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.Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, pp. 19–32. American Mathematical Society, Providence (1967)Google Scholar
- 31.Francez, N.: Fairness, Texts and Monographs in Computer Science, pp. 1–295. Springer, Berlin (1986)zbMATHCrossRefGoogle Scholar
- 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.Godefroid, P., Wolper, P.: A partial approach to model checking. In: Proceedings of LICS, pp. 406–415 (1991)Google Scholar
- 34.Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI, pp. 213–223 (2005)CrossRefGoogle Scholar
- 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.Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)zbMATHGoogle Scholar
- 37.Grosu, R., Smolka, S.A.: Monte Carlo model checking. In: Proceedings of TACAS, pp. 271–286 (2005)CrossRefGoogle Scholar
- 38.Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: Proceedings of Automated Software Engineering, November 2001, pp. 135–143 (2001)Google Scholar
- 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.Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)zbMATHCrossRefGoogle Scholar
- 41.Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)Google Scholar
- 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.Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)CrossRefGoogle Scholar
- 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.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.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.Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. EATCS Series, pp. 1–304. Springer, Berlin (2008)Google Scholar
- 48.Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Proceedings of CAV, pp. 172–183 (1999)CrossRefGoogle Scholar
- 49.Lamport, L.: “Sometimes” is sometimes “not never”. In: Proceedings of POPL, pp. 175–185 (1980)Google Scholar
- 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.Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Proceedings of RV, pp. 122–135 (2010)CrossRefGoogle Scholar
- 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.Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, Berlin (1991)Google Scholar
- 54.Mazurkiewicz, A.W.: Trace theory. In: Proceedings of Advances in Petri Nets, pp. 279–324 (1986)Google Scholar
- 55.McConnel, S.: Code Complete - A Practical Handbook of Software Construction, 2nd edn. Microsoft Press, Redmond (2004)Google Scholar
- 56.McMillan, K.L.: Interpolation and SAT-based model checking. In: Proceedings of CAV, pp. 1–13 (2003)Google Scholar
- 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.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.Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)Google Scholar
- 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.Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatic 6, 319–340 (1976)MathSciNetzbMATHCrossRefGoogle Scholar
- 62.Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Proceedings of CADE, pp. 748–752 (1992)CrossRefGoogle Scholar
- 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.Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46–57 (1977)Google Scholar
- 65.Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of POPL, pp. 179–190 (1989)Google Scholar
- 66.Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of FOCS, pp. 746–757 (1990)Google Scholar
- 67.Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. Symposium on Programming, pp. 337–351 (1982)Google Scholar
- 68.Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS, pp. 55–74 (2002)Google Scholar
- 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.Safra, S.: On the complexity of omega-automata. In: Proceedings of FOCS, pp. 319–327 (1988)Google Scholar
- 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.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.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.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.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.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.Walukiewicz, I.: Difficult configurations - on the complexity of LTrL. In: Proceedings of ICALP, pp. 140–151 (1998)CrossRefGoogle Scholar
- 78.Winskel, G.: Event structures. In: Proceedings of Advances in Petri Nets, pp. 325–392 (1986)CrossRefGoogle Scholar
- 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.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