Real-time monitoring for correctness and robustness

Abstract

The objective of this thesis is to develop a framework for real-time monitoring of Cyber-Physical System (CPS) designs for correctness and robustness and to offer verification methods applicable to real-scale industrial designs. We believe that runtime verification based on temporal logic provides a rigorous, systematic and efficient solution to the challenge of real-time monitoring. In order to integrate our monitors with modern Hardware-in-the-Loop (HiL) testbenches, we provide an algorithm for synthesizing qualitative monitors in hardware from safety properties expressed in Signal Temporal Logic (STL). By composing the monitor from basic temporal testers, we are able to parallelize the computation of the satisfaction verdict. Thus, we minimize computational delay and obtain responsive monitors which provide real-time correctness verdicts. Binary satisfaction verdicts may not be sufficient for properties evaluated against real-valued behaviors. The satisfaction relation can be replaced by a metric-based quantitative verdict which gives a finer measure of how robustly a behavior satisfies a specification. Typically, the development of such verdicts is driven by a specific type of requirements and behaviors. This resulted in a plethora of verdicts, each with its own definition and algorithm. We aim to define a uniform approach to precise robustness monitoring, by leveraging a common formalism for regular specifications over large ordered alphabets: symbolic automata (SA). By introducing algebraicallydefined weights into SA, we obtain a generic algorithm for monitoring both correctness and robustness. It provides verdicts which can be adapted to the desired class of behaviors simply by selecting the appropriate set of algebraic operations. Since the algorithm is based on dynamic programming it computes verdicts in real-time and admits direct hardware implementation. A typical CPS exploits digital processing units to control processes in physical environment. During the execution, a CPS exhibits complex behavior and generates execution traces. For evaluating conformance of CPS traces with the specification, we must consider trace discrepancies in value and time domain. In order to appropriately represent influences from both domains we define a robustness degree based on Weighted Edit Distance (WED). We demonstrate a real-time algorithm for computing WED-based robustness degree of traces of a serial protocol SENT, taken from the automotive domain. We conduct a large case study to assess benefits of using runtime monitors in an industrial setting and promote monitor reuse on different abstraction levels and product design phases. In order to apply the monitors to a class of asynchronous serial protocols, frequently used in the industry, we equip them with a procedure for error recovery and logging. The ability to self-recover allows to continue monitoring long data streams even after multiple requirement violations occur.