A Practical Approach to Runtime Verification
摘要
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.