Skip to main content
SpringerLink
Log in

A Retrospective Look at the Monitoring and Checking (MaC) Framework

  • Conference paper
  • First Online:
Runtime Verification (RV 2019)

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

Included in the following conference series:

Abstract

The Monitoring and Checking (MaC) project gave rise to a framework for runtime monitoring with respect to formally specified properties, which later came to be known as runtime verification. The project also built a pioneering runtime verification tool, Java-MaC, that was an instantiation of the approach to check properties of Java programs. In this retrospective, we discuss decisions made in the design of the framework and summarize lessons learned in the course of the project.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Alspaugh, T.A., Faulk, S.R., Britton, K.H., Parker, R.A., Parnas, D.L., Shore, J.E.: Software requirements for the A7-E aircraft. Technical report NRL Memorandum Report 3876, Naval Research Laboratory, August 1992

    Google Scholar 

  2. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20, 14:1–14:64 (2010)

    MATH  Google Scholar 

  3. Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200–225. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-92188-2_9

    Chapter  MATH  Google Scholar 

  4. Bhargavan, K., et al.: Verisim: formal analysis of network simulations. IEEE Trans. Software Eng. 28(2), 129–145 (2002). https://doi.org/10.1109/32.988495

    Article  Google Scholar 

  5. Blum, M., Kannan, S.: Designing programs that check their work. J. ACM 42, 269–291 (1995)

    Article  Google Scholar 

  6. Chadha, R., Sistla, A.P., Viswanathan, M.: On the expressiveness and complexity of randomization in finite state monitors. J. ACM 56(5), 26:1–26:44 (2009)

    Article  MathSciNet  Google Scholar 

  7. De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-53479-2_17

    Chapter  Google Scholar 

  8. Falcone, Y., Mariani, L., Rollet, A., Saha, S.: Runtime failure prevention and reaction. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 103–134. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_4

    Chapter  Google Scholar 

  9. Gordon, D., Spears, W., Sokolsky, O., Lee, I.: Distributed spatial control and global monitoring of mobile agents. In: Proceedings of the IEEE International Conference on Information, Intelligence, and Systems, November 1999

    Google Scholar 

  10. Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_24

    Chapter  MATH  Google Scholar 

  11. Heitmeyer, C.L.: Software cost reduction. In: Marciniak, J.J. (ed.) Encyclopedia of Software Engineering. Wiley, New York (2002)

    Google Scholar 

  12. Lee, I., Ben-Abdallah, H., Kannan, S., Kim, M., Sokolsky, O.: A monitoring and checking framework for run-time correctness assurance. In: Proceedings of the Korea-U.S. Technical Conference on Strategic Technologies, October 1998

    Google Scholar 

  13. Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Java-MaC: a run-time assurance tool for Java programs. In: Proceedings of Workshop on Runtime Verification (RV 2001). Electronic Notes in Theoretical Computer Science, vol. 55, July 2001

    Article  Google Scholar 

  14. Kim, M., Lee, I., Sammapun, U., Shin, J., Sokolsky, O.: Monitoring, checking, and steering of real-time systems. In: 2nd Workshop on Run-time Verification, July 2002

    Article  Google Scholar 

  15. Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., Sokolsky, O.: Formally specified monitoring of temporal properties. In: Proceedings of the European Conference on Real-Time Systems (ECRTS 1999), pp. 114–121, June 1999

    Google Scholar 

  16. Kini, D., Viswanathan, M.: Probabilistic automata for safety LTL specifications. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 118–136. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54013-4_7

    Chapter  Google Scholar 

  17. Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, June 1999

    Google Scholar 

  18. Peled, D., Havelund, K.: Refining the safety–liveness classification of temporal properties according to monitorability. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not?. LNCS, vol. 11200, pp. 218–234. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-22348-9_14

    Chapter  Google Scholar 

  19. Pettersson, O.: Execution monitoring in robotics: a survey. Robot. Auton. Syst. 53(2), 73–88 (2005)

    Article  MathSciNet  Google Scholar 

  20. Roohi, N., Kaur, R., Weimer, J., Sokolsky, O., Lee, I.: Parameter invariant monitoring for signal temporal logic. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control, pp. 187–196 (2018)

    Google Scholar 

  21. Sammapun, U., Lee, I., Sokolsky, O., Regehr, J.: Statistical runtime checking of probabilistic properties. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 164–175. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77395-5_14

    Chapter  Google Scholar 

  22. Sammapun, U.: Monitoring and checking of real-time and probabilistic properties. Ph.D. thesis, University of Pennsylvania (2007)

    Google Scholar 

  23. Sha, L.: Using simplicity to control complexity. IEEE Softw. 18(4), 20–28 (2001)

    Article  Google Scholar 

  24. Sokolsky, O., Sammapun, U., Lee, I., Kim, J.: Run-time checking of dynamic properties. In: Proceeding of the 5th International Workshop on Runtime Verification (RV 2005), Edinburgh, Scotland, UK, July 2005

    Google Scholar 

  25. Tan, L., Kim, J., Sokolsky, O., Lee, I.: Model-based testing and monitoring for hybrid embedded systems. In: Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration (IRI 2004), pp. 487–492, November 2004

    Google Scholar 

  26. Viswanathan, M., Kim, M.: Foundations for the run-time monitoring of reactive systems – Fundamentals of the MaC Language. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 543–556. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31862-0_38

    Chapter  Google Scholar 

  27. Yel, E., Bezzo, N.: Fast run-time monitoring, replanning, and recovery for safe autonomous system operations. In: Proceedings of the IEEE International Conference on Intelligent Robots and Systems (IROS), November 2019, to appear

    Google Scholar 

  28. Zhang, T., Eakman, G., Lee, I., Sokolsky, O.: Overhead-aware deployment of runtime monitors. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 375–381. Springer, Cham (2019)

    Google Scholar 

  29. Zhang, T., Eakman, G., Lee, I., Sokolsky, O.: Flexible monitor deployment for runtime verification of large scale software. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 42–50. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03427-6_6

    Chapter  Google Scholar 

  30. Zhou, C., Hansen, M.R.: Duration Calculus. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-06784-0

    Book  MATH  Google Scholar 

Download references

Acknowledgement

We would like to thank Dr. Ralph Wachter who provided and encouraged us with research funding and freedom to explore and develop the MaC framework when he was at the ONR. We also would like to thank other participants of the ONR MURI project: Andre Scedrov, John Mitchell, Ronitt Rubinfeld, Cynthia Dwork, for all the fruitful discussions. Recent extensions of our monitoring and checking approach have been funded by the DARPA Assured Autonomy program under contract FA8750-18-C-0090, and by the ONR contract N68335-19-C-0200. One of the authors of the first MaC paper [12], Hanêne Ben-Abdallah, participated in the project as a summer visitor in 1998.

Author information

Authors and Affiliations

  1. University of Pennsylvania, Philadelphia, USA

    Sampath Kannan, Insup Lee & Oleg Sokolsky

  2. KAIST, Daejeon, Republic of Korea

    Moonzoo Kim

  3. University of Illinois, Urbana-Champaign, USA

    Mahesh Viswanathan

Authors
  1. Sampath Kannan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Moonzoo Kim
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Insup Lee
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Oleg Sokolsky
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Mahesh Viswanathan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Oleg Sokolsky .

Editor information

Editors and Affiliations

  1. Universität des Saarlandes, Saarbrücken, Germany

    Bernd Finkbeiner

  2. University of Milano Bicocca, Milan, Italy

    Leonardo Mariani

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kannan, S., Kim, M., Lee, I., Sokolsky, O., Viswanathan, M. (2019). A Retrospective Look at the Monitoring and Checking (MaC) Framework. In: Finkbeiner, B., Mariani, L. (eds) Runtime Verification. RV 2019. Lecture Notes in Computer Science(), vol 11757. Springer, Cham. https://doi.org/10.1007/978-3-030-32079-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32079-9_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32078-2

  • Online ISBN: 978-3-030-32079-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation