{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T09:33:19Z","timestamp":1766050399007,"version":"3.28.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,7,11]],"date-time":"2023-07-11T00:00:00Z","timestamp":1689033600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,11]],"date-time":"2023-07-11T00:00:00Z","timestamp":1689033600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Deutsches Zentrum f\u00fcr Luft- und Raumfahrt e. V. (DLR)"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 the correctness of the monitor. In this paper, we present a verification extension to the<jats:sc>Lola<\/jats:sc>monitoring language that extends 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<jats:sc>SMT<\/jats:sc>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 specifications. The errors range from incorrect default values in offset computations to complex algorithmic errors that result in unexpected temporal patterns. We also report how verified specifications can be monitored efficiently at runtime.<\/jats:p>","DOI":"10.1007\/s10009-023-00712-3","type":"journal-article","created":{"date-parts":[[2023,7,11]],"date-time":"2023-07-11T13:01:36Z","timestamp":1689080496000},"page":"593-616","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Monitoring with verified guarantees"],"prefix":"10.1007","volume":"25","author":[{"given":"Jan","family":"Baumeister","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johann C.","family":"Dauer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Schirmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,11]]},"reference":[{"issue":"5s","key":"712_CR1","doi-asserted-by":"publisher","DOI":"10.1145\/3358220","volume":"18","author":"J. Baumeister","year":"2019","unstructured":"Baumeister, J., Finkbeiner, B., Schwenger, M., Torfah, H.: FFGA stream-monitoring of real-time properties. ACM Trans. Embed. Comput. Syst. 18(5s), 88 (2019). https:\/\/doi.org\/10.1145\/3358220","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"712_CR2","first-page":"451","volume-title":"Runtime Verification","author":"J. Baumeister","year":"2020","unstructured":"Baumeister, J., Finkbeiner, B., Kruse, M., Schwenger, M.: Automatic optimizations for stream-based monitoring languages. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) Runtime Verification, pp.\u00a0451\u2013461. Springer, Cham (2020)"},{"key":"712_CR3","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-030-53291-8_3","volume-title":"Computer Aided Verification","author":"J. Baumeister","year":"2020","unstructured":"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.) Computer Aided Verification, pp.\u00a028\u201339. Springer, Cham (2020)"},{"key":"712_CR4","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69061-0","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS, vol.\u00a04334. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-69061-0"},{"key":"712_CR5","doi-asserted-by":"crossref","first-page":"425","DOI":"10.7551\/mitpress\/5641.003.0021","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","author":"G. Berry","year":"2000","unstructured":"Berry, G.: The foundations of ESTEREL. In: Proof, Language and Interaction: Essays in Honour of Robin Milner, pp.\u00a0425\u2013454. MIT Press, Cambridge (2000)"},{"key":"712_CR6","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/s10009-014-0314-5","volume":"17","author":"F. Bobot","year":"2015","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Let\u2019s verify this with why3. Int. J. Softw. Tools Technol. Transf. 17, 709\u2013727 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"712_CR7","unstructured":"Cluzeau, J.M., Henriquel, X., van Dijk, L., Gronskiy, A.: Concepts of design assurance for neural networks (CoDANN). Tech. Rep., EASA European Union Aviation Safety Agency (Mar 2020)"},{"key":"712_CR8","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1109\/TIME.2005.26","volume-title":"12th International Symposium on Temporal Representation and Reasoning (TIME\u201905)","author":"B. D\u2019Angelo","year":"2005","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME\u201905), pp.\u00a0166\u2013174 (2005). https:\/\/doi.org\/10.1109\/TIME.2005.26"},{"key":"712_CR9","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-030-88494-9_4","volume-title":"Runtime Verification","author":"J.C. Dauer","year":"2021","unstructured":"Dauer, J.C., Finkbeiner, B., Schirmer, S.: Monitoring with verified guarantees. In: Feng, L., Fisman, D. (eds.) Runtime Verification, pp.\u00a062\u201380. Springer, Cham (2021)"},{"key":"712_CR10","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-319-46982-9_10","volume-title":"Runtime Verification","author":"P. Faymonville","year":"2016","unstructured":"Faymonville, P., Finkbeiner, B., Schirmer, S., Torfah, H.: A stream-based specification language for network monitoring. In: Falcone, Y., S\u00e1nchez, C. (eds.) Runtime Verification, pp.\u00a0152\u2013168. Springer, Cham (2016)"},{"key":"712_CR11","first-page":"431","volume-title":"Runtime Verification","author":"B. Finkbeiner","year":"2020","unstructured":"Finkbeiner, B., Oswald, S., Passing, N., Schwenger, M.: Verified rust monitors for lola specifications. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) Runtime Verification, pp.\u00a0431\u2013450. Springer, Cham (2020)"},{"key":"712_CR12","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-94-011-1793-7_4","volume-title":"Program Verification","author":"R.W. Floyd","year":"1993","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Program Verification, pp.\u00a065\u201381. Springer, Dordrecht (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4"},{"key":"712_CR13","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/3-540-18317-5_15","volume-title":"Functional Programming Languages and Computer Architecture","author":"T. Gautier","year":"1987","unstructured":"Gautier, T., Le Guernic, P., Besnard, L.: SIGNAL: a declarative language for synchronous programming of real-time systems. In: Kahn, G. (ed.) Functional Programming Languages and Computer Architecture, pp.\u00a0257\u2013277. Springer, Berlin (1987)"},{"key":"712_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/FMCAD.2008.ECP.19","volume-title":"2008 Formal Methods in Computer-Aided Design","author":"G. Hagen","year":"2008","unstructured":"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.\u00a01\u20139 (2008). https:\/\/doi.org\/10.1109\/FMCAD.2008.ECP.19"},{"issue":"9","key":"712_CR15","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305\u20131320 (1991). https:\/\/doi.org\/10.1109\/5.97300","journal-title":"Proc. IEEE"},{"issue":"10","key":"712_CR16","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"712_CR17","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-60045-0_45","volume-title":"Computer Aided Verification","author":"L.J. Jagadeesan","year":"1995","unstructured":"Jagadeesan, L.J., Puchol, C., Von Olnhausen, J.E.: Safety property verification of ESTEREL programs and applications to telecommunications software. In: Wolper, P. (ed.) Computer Aided Verification, pp.\u00a0127\u2013140. Springer, Berlin (1995)"},{"key":"712_CR18","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp.\u00a0348\u2013370. Springer, Berlin (2010)"},{"key":"712_CR19","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation, pp.\u00a041\u201362. Springer, Berlin (2016)"},{"key":"712_CR20","unstructured":"Nagarajan, P., Kannan, S.K., Torens, C., Vukas, M.E., Wilber, G.F.: ASTM F3269 \u2013 an Industry Standard on Run Time Assurance for Aircraft Systems. https:\/\/arc.aiaa.org\/doi\/abs\/10.2514\/6.2021-0525"},{"key":"712_CR21","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-23820-3_2","volume-title":"Runtime Verification","author":"L. Nenzi","year":"2015","unstructured":"Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Bartocci, E., Majumdar, R. (eds.) Runtime Verification, pp.\u00a021\u201337. Springer, Cham (2015)"},{"key":"712_CR22","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-16612-9_26","volume-title":"Runtime Verification","author":"L. Pike","year":"2010","unstructured":"Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Verification, pp.\u00a0345\u2013359. Springer, Berlin (2010)"},{"key":"712_CR23","unstructured":"Reactive Systems\u00a0Group, C.: RTLola. https:\/\/github.com\/reactive-systems\/RTLola-Frontend, https:\/\/github.com\/reactive-systems\/RTLola-Interpreter (2023)"},{"key":"712_CR24","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-54862-8_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Reinbacher","year":"2014","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a0357\u2013372. Springer, Berlin (2014)"},{"key":"712_CR25","unstructured":"Schirmer, S.: Runtime monitoring with Lola. Master\u2019s thesis, Saarland University (Dec. 2016)"},{"key":"712_CR26","volume-title":"2018 AIAA Information Systems-AIAA Infotech @ Aerospace","author":"S. Schirmer","year":"2018","unstructured":"Schirmer, S., Torens, C., Adolf, F.: Formal monitoring of risk-based geofences. In: 2018 AIAA Information Systems-AIAA Infotech @ Aerospace (2018). https:\/\/arc.aiaa.org\/doi\/abs\/10.2514\/6.2018-1986"},{"key":"712_CR27","doi-asserted-by":"publisher","first-page":"3504","DOI":"10.1109\/ACC.1998.703255","volume-title":"Proceedings of the 1998 American Control Conference. ACC (IEEE Cat. No.98CH36207)","author":"D. Seto","year":"1998","unstructured":"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.\u00a06, pp.\u00a03504\u20133508 (1998). https:\/\/doi.org\/10.1109\/ACC.1998.703255"},{"key":"712_CR28","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-030-67067-2_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Song","year":"2021","unstructured":"Song, Y., Chin, W.N.: A synchronous effects logic for temporal verification of pure ESTEREL. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation, pp.\u00a0417\u2013440. Springer, Cham (2021)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00712-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-023-00712-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00712-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T23:37:40Z","timestamp":1729726660000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-023-00712-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,11]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,8]]}},"alternative-id":["712"],"URL":"https:\/\/doi.org\/10.1007\/s10009-023-00712-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2023,7,11]]},"assertion":[{"value":"30 May 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 July 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}