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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
In its original version the data is separated into assured and unassured data and data preparation components are added.
- 3.
- 4.
References
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
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
Berry, G.: The Foundations of Esterel, pp. 425–454. MIT Press, Cambridge (2000)
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
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
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
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
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
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
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
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259
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
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
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
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
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
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
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
Schirmer, S.: Runtime monitoring with Lola. Master’s thesis, Saarland University, December 2016
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
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
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
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
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)