Runtime Verification for Rigorous Engineering and Safe Operation of IoT
Gastbeitrag von Dejan Ničković, AIT
From Industry 4.0 and smart manufacturing to remote healthcare – rapidly proliferating Internet-of-Thing (IoT) applications are becoming pervasive in every aspect of our daily lives. IoT applications consist of physical entities that are interconnected with sensors, actuators, software and other technologies that interact with the physical environment, while processing and exchanging data with other devices over the Internet. IoT applications are evolving to be tremendously complex systems that can operate in sophisticated and unpredictable environments.
Many IoT applications are safety-critical and faults can have catastrophic consequences involving significant material damage or even loss of human lives. Therefore, verification and validation (V&V) for IoT is essential to achieve high standards with respect to safety requirements. Due to its complexity, exhaustive verification of IoT applications at the design time is virtually impossible and must be complemented with techniques applied during the operation of the system.
Runtime verification (RV), also known as runtime monitoring and illustrated in Figure 1, is an alternative approach for ensuring the safe operation of complex systems that cannot be statically verified. RV is a light-weight verification technique that combines formal specifications with the evaluation of individual system behaviors. When applied to an IoT system under operation, RV provides a reliable, rigorous and systematic way of finding property violations in real time and possibly taking a corrective action.
Fig. 1. Runtime verification architecture
RV can also be applied during the (model-based) design of IoT where behaviors correspond to simulation traces. In this context, monitoring can be viewed as part of the simulation-based V&V process, which gives up the complete coverage associated with verification, but still uses a rigorous mathematical specification language to classify behaviors.
In the past years, we worked on various aspects of RV applied to IoT and cyber-physical systems (CPS): (1) formal specification languages for RV, (2) RV algorithms and tools, and (3) additional analysis methods that use RV as basic technology.
We introduced Signal Temporal Logic (STL) [1], a specification language for expressing real-time temporal safety properties of IoT and CPS. STL allows to measure how far an observed signal is from satisfying or violating its specification. We developed methods for offline, online and real-time monitoring of STL specifications, using both qualitative and quantitative evaluation: (1) a translation from STL to monitors implemented on FPGA, (2) the rtamt[1] Python library for monitoring STL specifications, (3) that we integrated to the Robotic Operating System (ROS)[2] and MathWorks MATLAB/Simulink model-based development environments [2]. We finally used STL monitors to develop applications beyond RV for rigorous engineering of IoT and CPS. We developed search-based testing procedures that combine quantitative monitors with global optimization to efficiently find system failures [3]. We also devised methods for explaining and localizing faults in complex systems guided by STL specifications [4].
RV is a powerful and versatile technology that can be applied both during the design-time of a complex system as well as during its operation, facilitating the design-operation continuum. In addition to its ability to efficiently detect failures, RV can be used to develop other analysis procedures that support rigorous engineering of IoT.
References:
[1] Oded Maler, Dejan Nickovic: Monitoring Temporal Properties of Continuous Signals. FORMATS/FTRTFT 2004: 152-166.
[2] Dejan Nickovic, Tomoya Yamaguchi: RTAMT: Online Robustness Monitors from STL. ATVA 2020: 564-571.
[3] Thomas Ferrère, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, James Kapinski: Interface-aware signal temporal logic. HSCC 2019: 57-66.
[4] Ezio Bartocci, Niveditha Manjunath, Leonardo Mariani, Cristinel Mateis, Dejan Nickovic: Automatic Failure Explanation in CPS Models. SEFM 2019: 69-86.
mehr erfahren
