2021/11/10 by Niklas Metzger, Metzger, Niklas, Sanny Schmitt +3
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Software Reliability and Analysis Research #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2111.05613
openalex publication_date 2021/11/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The verification of cyber-physical systems operating in a safety-critical environment requires formal system models. The validity of the verification hinges on the precision of the model: possible behavior not captured in the model can result in formally verified, but unsafe systems. Yet, manual construction is delicate and error-prone while automatic construction does not scale for large and complex systems. As a remedy, this paper devises an automatic construction algorithm that utilizes information contained in artifacts of the development process: a runtime monitoring specification and recorded test traces. These artifacts incur no additional cost and provide sufficient information so that the construction process scales well for large systems. The algorithm uses a hybrid approach between a top-down and a bottom-up construction which allows for proving the result conservative, while limiting the level of over-approximation.