Top

Published in:

2019 | OriginalPaper | Chapter

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

Authors : Sampath Kannan, Moonzoo Kim, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan

Published in: Runtime Verification

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

next chapter Introspective Environment Modeling

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

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

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_9CrossRefMATH

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.988495CrossRef

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

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)MathSciNetCrossRef

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_17CrossRef

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_4CrossRef

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

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_24CrossRefMATH

11.

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

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

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 2001CrossRef

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 2002CrossRef

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

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_7CrossRef

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

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_14CrossRef

19.

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

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)

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_14CrossRef

22.

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

23.

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

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

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

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_38CrossRef

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

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)

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_6CrossRef

30.

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

Title: A Retrospective Look at the Monitoring and Checking (MaC) Framework
Authors: Sampath Kannan
Moonzoo Kim
Insup Lee
Oleg Sokolsky
Mahesh Viswanathan
Publisher: Springer International Publishing
Book: Runtime Verification
Print ISBN: 978-3-030-32078-2

Electronic ISBN: 978-3-030-32079-9

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-32079-9_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner