Skip to main content
Springer Nature Link
Log in

Combining Monitoring with Run-Time Assertion Checking

  • Chapter
Formal Methods for Executable Software Models (SFM 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8483))

Abstract

According to a study in 2002 commisioned by a US Department, software bugs annually costs the US economy an estimated $59 billion. A more recent study in 2013 by Cambridge University estimated that the global cost has risen to $312 billion globally.

There exists various ways to prevent, isolate and fix software bugs, ranging from lightweight methods that are (semi)-automatic, to heavyweight methods that require significant user interaction. Our own method described in this tutorial is based on automated run-time checking of a combination of protocol- and data-oriented properties of object-oriented programs.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.): Communicating Sequential Processes. LNCS, vol. 3525. Springer, Heidelberg (2005)

    Google Scholar 

  2. Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA, pp. 345–364 (2005)

    Google Scholar 

  3. Artho, C., Drusinksy, D., Goldberg, A., Havelund, K., Lowry, M., Păsăreanu, C.S., Roşu, G., Visser, W.: Experiments with test case generation and runtime analysis. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 87–107. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Backus, J.W.: The syntax and semantics of the proposed international algebraic language of the Zurich ACM-GAMM conference. In: IFIP Congress, pp. 125–131 (1959)

    Google Scholar 

  5. Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes, 1st edn. Cambridge University Press, New York (2009)

    Book  MATH  Google Scholar 

  6. Bartetzko, D., Fischer, C., Möller, M., Wehrheim, H.: Jass - Java with assertions. Electr. Notes Theor. Comput. Sci. 55(2) (2001)

    Google Scholar 

  7. Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651–674 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  8. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  9. Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal — a tool suite for automatic verification of real–time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  10. Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Berdine, J., Cook, B., Ishtiaq, S.: sLAyer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  12. Bergstra, J.A., Klop, J.W.: Acttau: A universal axiom system for process specification. In: Algebraic Methods, pp. 447–463 (1987)

    Google Scholar 

  13. Bertot, Y., Castéran, P., Huet, G., Paulin-Mohring, C.: Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin (2004)

    Google Scholar 

  14. Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer 7(3), 212–232 (2005)

    Article  Google Scholar 

  15. Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Chalin, P., James, P.R., Karabotsos, G.: JML4: Towards an industrial grade IVE for java and next generation research platform for JML. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 70–83. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Chen, F., Rosu, G.: MOP: an efficient and generic runtime verification framework. In: OOPSLA, pp. 569–588 (2007)

    Google Scholar 

  18. Cheon, Y., Perumandla, A.: Specifying and checking method call sequences of Java programs. Software Quality Journal 15(1), 7–25 (2007)

    Article  Google Scholar 

  19. Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  20. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  21. Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)

    Google Scholar 

  22. Colombo, C., Pace, G.J., Schneider, G.: LARVA — safer monitoring of real-time java programs (tool paper). In: SEFM, pp. 33–37 (2009)

    Google Scholar 

  23. Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001)

    Article  MATH  Google Scholar 

  24. de Boer, F.S., Bonsangue, M.M., Steffen, M., Ábrahám, E.: A fully abstract semantics for UML components. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 49–69. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  25. de Gouw, S., de Boer, F.S., Johnsen, E.B., Wong, P.Y.H.: Run-time checking of data- and protocol-oriented properties of Java programs: an industrial case study. In: SAC, pp. 1573–1578 (2013)

    Google Scholar 

  26. Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA, pp. 213–226 (2008)

    Google Scholar 

  27. Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  28. Fischer, C., Wehrheim, H.: Behavioural subtyping relations for Object-Oriented formalisms. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 469–483. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  29. Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, Providence, Rhode Island. Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society (1967)

    Google Scholar 

  30. Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-Dimensional Modal Logics: Theory and Applications. Elsevier (2003)

    Google Scholar 

  31. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Elements of Reusable Object-Oriented Software. Addison-Wesley (1995)

    Google Scholar 

  32. Grune, D., Jacobs, C.J.: Parsing Techniques - A Practical Guide, 2nd edn. Springer (2008)

    Google Scholar 

  33. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    Google Scholar 

  34. Hedin, G.: Incremental attribute evaluation with side-effects. In: Hammer, D. (ed.) CCHSC 1988. LNCS, vol. 371, pp. 175–189. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  35. Heisel, M., Reif, W., Stephan, W.: Implementing verification strategies in the KIV-system. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 131–140. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  36. Hennessy, M.: Algebraic theory of processes. MIT Press series in the foundations of computing. MIT Press (1988)

    Google Scholar 

  37. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  38. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  39. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)

    Google Scholar 

  40. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)

    Article  Google Scholar 

  41. International Telecommunication Union. ITU-T Recommendation Z.120: Message Sequence Chart (MSC). Technical report, ITU, Geneva (2001)

    Google Scholar 

  42. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  43. Jeffrey, A., Rathke, J.: ava Jr: Fully abstract trace semantics for a core Java language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 423–438. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  44. Kleene, S.C.: Representation of events in nerve nets and finite automata. Automata Studies (1956)

    Google Scholar 

  45. Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Prog. Lang. Syst. 28(4), 619–695 (2006)

    Article  Google Scholar 

  46. Klint, P., van der Storm, T., Vinju, J.J.: Rascal: a domain specific language for source code analysis and manipulation. In: Walenstein, A., Schupp, S. (eds.) Proceedings of the IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2009), pp. 168–177 (2009)

    Google Scholar 

  47. Knuth, D.E.: Semantics of context-free languages. Mathematical Systems Theory 2(2), 127–145 (1968)

    Article  MathSciNet  MATH  Google Scholar 

  48. Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)

    Google Scholar 

  49. Lee, L.: Fast context-free grammar parsing requires fast boolean matrix multiplication. J. ACM 49(1), 1–15 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  50. Li, X., Liu, Z., He, J.: A formal semantics of UML sequence diagram. In: Australian Software Engineering Conference, pp. 168–177 (2004)

    Google Scholar 

  51. Martin, J.C.: Introduction to Languages and The Theory of Computation. McGraw-Hil (2010)

    Google Scholar 

  52. Martin, M., Livshits, B., Lam, M.S.: Finding application errors and security flaws using PQL: a Program Query Language. In: OOPLSLA (2005)

    Google Scholar 

  53. Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall (1997)

    Google Scholar 

  54. Mikhajlov, L., Sekerinski, E.: A study of the fragile base class problem. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 355–382. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  55. Milner, R.: Fully abstract models of typed λ-calculi. Theoretical Comput. Sci. 4, 1–22 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  56. Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    Book  MATH  Google Scholar 

  57. Milner, R.: Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, New York (1999)

    MATH  Google Scholar 

  58. Nobakht, B., Bonsangue, M.M., de Boer, F.S., de Gouw, S.: Monitoring method call sequences using annotations. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 53–70. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  59. Parr, T.J., Quong, R.W.: Adding semantic and syntactic predicates to LL(k): pred-LL(k). In: Fritzson, P.A. (ed.) CC 1994. LNCS, vol. 786, pp. 263–277. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  60. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57 (1977)

    Google Scholar 

  61. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  62. Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: FOCS, pp. 109–121 (1976)

    Google Scholar 

  63. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)

    Google Scholar 

  64. Sangiorgi, D., Walker, D.: The Pi-Calculus - a theory of mobile processes. Cambridge University Press (2001)

    Google Scholar 

  65. Sipser, M.: Introduction to the theory of computation. PWS Publishing Company (1997)

    Google Scholar 

  66. Stolz, V., Huch, F.: Runtime verification of concurrent Haskell programs. Electr. Notes Theor. Comput. Sci. 113, 201–216 (2005)

    Article  Google Scholar 

  67. Valiant, L.G.: General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10(2), 308–315 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  68. van den Berg, J., Jacobs, B.: The LOOP Compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  69. van Eijk, P.H.J., Vissers, C., Diaz, M. (eds.): Formal Description Technique Lotos: Results of the Esprit Sedos Project. Elsevier Science Inc., New York (1989)

    Google Scholar 

  70. Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, Amsterdam, The Netherlands

    Frank S. de Boer & Stijn de Gouw

  2. Leiden University, The Netherlands

    Frank S. de Boer & Stijn de Gouw

Authors
  1. Frank S. de Boer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stijn de Gouw
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Scienze di Base e Fondamenti, Università di Urbino, Piazza della Republica 13, 61029, Urbino, Italy

    Marco Bernardo

  2. Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Ferruccio Damiani

  3. Fachbereich Informatik, Technische Universität Darmstadt, Hochschulstraße 10, 64289, Darmstadt, Germany

    Reiner Hähnle

  4. Department of Informatics, University of Oslo, P.O. Box 1080 Blindern, 0316, Oslo, Norway

    Einar Broch Johnsen

  5. Institut für Softwaretechnik und Fahrzeuginformatik, Technische Universität Braunschweig, Mühlenpfordtstraße 23, 38106, Braunschweig, Germany

    Ina Schaefer

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this chapter

Cite this chapter

de Boer, F.S., de Gouw, S. (2014). Combining Monitoring with Run-Time Assertion Checking. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds) Formal Methods for Executable Software Models. SFM 2014. Lecture Notes in Computer Science, vol 8483. Springer, Cham. https://doi.org/10.1007/978-3-319-07317-0_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-07317-0_6

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-07316-3

  • Online ISBN: 978-3-319-07317-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics