Skip to main content
SpringerLink
Log in

Monitoring with Verified Guarantees

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

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

Included in the following conference series:

Abstract

Runtime monitoring is generally considered a light-weight alternative to formal verification. In safety-critical systems, however, the monitor itself is a critical component. For example, if the monitor is responsible for initiating emergency protocols, as proposed in a recent aviation standard, then the safety of the entire system critically depends on guarantees of the correctness of the monitor. In this paper, we present a verification extension to the Lola monitoring language that integrates the efficient specification of the monitor with Hoare-style annotations that guarantee the correctness of the monitor specification. We add two new operators, assume and assert, which specify assumptions of the monitor and expectations on its output, respectively. The validity of the annotations is established by an integrated SMT solver. We report on experience in applying the approach to specifications from the avionics domain, where the annotation with assumptions and assertions has lead to the discovery of safety-critical errors in the specifications. The errors range from incorrect default values in offset computations to complex algorithmic errors that result in unexpected temporal patterns.

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 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.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

Similar content being viewed by others

Notes

  1. 1.

    https://www.dlr.de/content/en/research-facilities/superartis-en.html.

  2. 2.

    In its original version the data is separated into assured and unassured data and data preparation components are added.

  3. 3.

    https://rtlola.org/.

  4. 4.

    https://docs.rs/z3/0.9.0/z3/.

References

  1. Baumeister, J., Finkbeiner, B., Schirmer, S., Schwenger, M., Torens, C.: RTLola cleared for take-off: monitoring autonomous aircraft. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 28–39. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_3

    Chapter  Google Scholar 

  2. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. Lecture Notes in Computer Science, vol. 4334. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69061-0

    Book  Google Scholar 

  3. Berry, G.: The Foundations of Esterel, pp. 425–454. MIT Press, Cambridge (2000)

    Google Scholar 

  4. Cluzeau, J.M., Henriquel, X., van Dijk, L., Gronskiy, A.: Concepts of design assurance for neural networks (CoDANN). Technical report, EASA European Union Aviation Safety Agency, March 2020

    Google Scholar 

  5. D’Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166–174 (2005). https://doi.org/10.1109/TIME.2005.26

  6. Finkbeiner, B., Oswald, S., Passing, N., Schwenger, M.: Verified rust monitors for Lola specifications. In: Deshmukh, J., Ničković, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 431–450. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-60508-7_24

    Chapter  Google Scholar 

  7. Floyd, R.W.: Assigning meanings to programs. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Program Verification, vol. 14, pp. 65–81. Springer, Dordrecht (1993). https://doi.org/10.1007/978-94-011-1793-7_4

    Chapter  Google Scholar 

  8. Gautier, T., Le Guernic, P., Besnard, L.: SIGNAL: a declarative language for synchronous programming of real-time systems. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol. 274, pp. 257–277. Springer, Heidelberg (1987). https://doi.org/10.1007/3-540-18317-5_15

    Chapter  Google Scholar 

  9. Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: 2008 Formal Methods in Computer-Aided Design, pp. 1–9 (2008). https://doi.org/10.1109/FMCAD.2008.ECP.19

  10. Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language Lustre. Proc. IEEE 79(9), 1305–1320 (1991). https://doi.org/10.1109/5.97300

    Article  Google Scholar 

  11. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259

    Article  MATH  Google Scholar 

  12. 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). https://doi.org/10.1007/978-3-642-20398-5_4

    Chapter  Google Scholar 

  13. Jagadeesan, L.J., Puchol, C., Von Olnhausen, J.E.: Safety property verification of Esterel programs and applications to telecommunications software. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 127–140. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60045-0_45

    Chapter  Google Scholar 

  14. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20

    Chapter  MATH  Google Scholar 

  15. Nagarajan, P., Kannan, S.K., Torens, C., Vukas, M.E., Wilber, G.F.: ASTM F3269 - an industry standard on run time assurance for aircraft systems. https://doi.org/10.2514/6.2021-0525

  16. Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 21–37. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_2

    Chapter  Google Scholar 

  17. Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 345–359. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_26

    Chapter  Google Scholar 

  18. Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357–372. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_24

    Chapter  Google Scholar 

  19. Schirmer, S.: Runtime monitoring with Lola. Master’s thesis, Saarland University, December 2016

    Google Scholar 

  20. Schirmer, S., Torens, C., Adolf, F.: Formal monitoring of risk-based geofences. https://doi.org/10.2514/6.2018-1986. https://arc.aiaa.org/doi/abs/10.2514/6.2018-1986

  21. Seto, D., Krogh, B., Sha, L., Chutinan, A.: The simplex architecture for safe online control system upgrades. In: Proceedings of the 1998 American Control Conference. ACC (IEEE Cat. No.98CH36207), vol. 6, pp. 3504–3508 (1998). https://doi.org/10.1109/ACC.1998.703255

  22. Song, Y., Chin, W.-N.: A synchronous effects logic for temporal verification of pure Esterel. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 417–440. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-67067-2_19

    Chapter  Google Scholar 

Download references

Acknowledgement

This work was partially supported by the German Research Foundation (DFG) as part of the Collaborative Research Center Foundations of Perspicuous Software Systems (TRR 248, 389792660), by the European Research Council (ERC) Grant OSARES (No. 683300), and by the Aviation Research Programm LuFo of the German Federal Ministry for Economic Affairs and Energy as part of “Volocopter Sicherheits-Technologie zur robusten eVTOL Flugzustandsabsicherung durch formales Monitoring” (No. 20Q1963C).

Author information

Authors and Affiliations

  1. German Aerospace Center (DLR), Braunschweig, Germany

    Johann C. Dauer & Sebastian Schirmer

  2. Helmholtz Center for Information Security (CISPA), Saarbrücken, Germany

    Bernd Finkbeiner

Authors
  1. Johann C. Dauer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernd Finkbeiner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sebastian Schirmer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sebastian Schirmer .

Editor information

Editors and Affiliations

  1. University of Virginia, Charlottesville, VA, USA

    Lu Feng

  2. Ben-Gurion University of the Negev, Be'er Sheva, Israel

    Dana Fisman

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Dauer, J.C., Finkbeiner, B., Schirmer, S. (2021). Monitoring with Verified Guarantees. In: Feng, L., Fisman, D. (eds) Runtime Verification. RV 2021. Lecture Notes in Computer Science(), vol 12974. Springer, Cham. https://doi.org/10.1007/978-3-030-88494-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-88494-9_4

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation