A Practical Approach to Runtime Verification

TitleA Practical Approach to Runtime Verification
Publication TypeConference Paper
Year of Publication2025
AuthorsHipler, R, Kallwies, H, Leucker, M, van Dommele, KGillian, Wien, J
Conference Name25th International Conference on Runtime Verification (RV)
Date Published09/2025
PublisherSpringer
Conference LocationGraz, Austria
KeywordsRequirement Syntax, Runtime verification, Software Testing, TeSSLa
Abstract

Runtime Verification (RV) is a formal method used to check whether the execution of a system adheres to a given specification. While extensive research has focused on developing foundational theories and tools—as well as domain-specific applications, such as in the space or automotive industries—the benefits of RV in the context of general-purpose software system development remain relatively underexplored. In this paper, we propose a flexible and generic workflow for integrating RV into the development and verification processes of general-purpose software systems. We designed and implemented a prototypical RV framework based on TeSSLa, a stream-based runtime verification specification language, to monitor elicited requirements. Our approach was applied in a case study on ValiBridge, an internal software tool developed by Infineon Austria to facilitate information exchange among stakeholders involved in post-silicon verification, where it was able to detect a previously unknown bug in the software. We analyze the impact of the RV setup on development efficiency and compare its effectiveness against an existing unit test suite.

URLhttps://link.springer.com/chapter/10.1007/978-3-032-05435-7_21
DOI10.1007/978-3-032-05435-7_21
Bibtex: 
@inproceedings {1496,
	title = {A Practical Approach to Runtime Verification},
	booktitle = {25th International Conference on Runtime Verification (RV)},
	year = {2025},
	month = {09/2025},
	publisher = {Springer},
	organization = {Springer},
	address = {Graz, Austria},
	abstract = {<p>Runtime Verification (RV) is a formal method used to check whether the execution of a system adheres to a given specification. While extensive research has focused on developing foundational theories and tools{\textemdash}as well as domain-specific applications, such as in the space or automotive industries{\textemdash}the benefits of RV in the context of general-purpose software system development remain relatively underexplored. In this paper, we propose a flexible and generic workflow for integrating RV into the development and verification processes of general-purpose software systems. We designed and implemented a prototypical RV framework based on TeSSLa, a stream-based runtime verification specification language, to monitor elicited requirements. Our approach was applied in a case study on ValiBridge, an internal software tool developed by Infineon Austria to facilitate information exchange among stakeholders involved in post-silicon verification, where it was able to detect a previously unknown bug in the software. We analyze the impact of the RV setup on development efficiency and compare its effectiveness against an existing unit test suite.</p>
},
	keywords = {Requirement Syntax, Runtime verification, Software Testing, TeSSLa},
	doi = {10.1007/978-3-032-05435-7_21},
	url = {https://link.springer.com/chapter/10.1007/978-3-032-05435-7_21},
	author = {Raik Hipler and Hannes Kallwies and Martin Leucker and Kevin Gillian van Dommele and Jannis Wien}
}