Cyber-Physical Systems (CPS) are systems with tight integration of computation, communication, and physical processes. These systems are the basis of many contemporary application domains, including transportation, military, health care, and robotics [1]. A significant number of CPS are also considered safety-critical systems, indicating that failures in such systems could cause loss of lives, property damage, or catastrophic environmental accidents [2].
Guaranteeing that such complex systems do not fail is a challenging task that goes hand to hand with safety standards. To assist the safe and secure development of CPS, tools based on formal methods (rigorous logical and mathematical techniques) have been used to specify, develop, and verify a wide range of system properties. Such tools can offer proofs or evidence about specific aspects and reveal inconsistencies, ambiguities, and incompleteness commonly overlooked by traditional testing procedures.
Formal verification [3] is one of the main ways formal methods are applied in the development of CPS, being present in several safety standards either as a suggestion or a mandatory requirement (e.g., ISO 26262, ISO/SAE 21434 in the automotive domain). It consists of comparing system behavior against a formal specification that rigorously describes the expected system’s correct operation. Formal verification techniques are classified into static and runtime verification. Static verification consists of exhaustively checking all possible behaviors of a system by performing a state-space search looking for the satisfaction of properties in all possible executions. By being so detailed in its process, this approach commonly faces the infamous state explosion problem. Such limitation usually translates to inconclusive results or forces the verification process to happen based on a much less detailed system model.
Runtime Verification (RV) [4] complements static formal verification techniques by analyzing, during runtime, carefully selected events of the system under scrutiny (SUS). These events reflect the system’s current state and serve as data to be analyzed by formally generated lightweight pieces of code, named monitors, instrumented alongside the SUS. By checking only a subset of the system’s events, RV can produce timely and precise verdicts about the compliance of a system’s run concerning its formal specification. RV also helps to close the gap between theoretical models and real systems and can speed up testing scenarios that would be tricky to reproduce under usual testing conditions.
Despite its benefits, RV introduces an inevitable and non-neglectable performance overhead in the SUS. If not correctly considered, such performance overhead could disrupt some of the system’s safety requirements (e.g., task scheduling). On top of that, the coupling of monitoring solutions could affect functional properties as well as non-functional properties like security and privacy if no formal approach is followed during its integration with the SUS [5].
In the context of the VALU3S project, a framework named MARS is being developed to aid in safely coupling runtime monitors in CPS. MARS’ planed contribution is twofold: on the one hand, it aims at facilitating the work of developers and engineers when it comes to designing applications with RV in mind by abstracting away unnecessary aspects during the specification of monitoring architectures. On the other hand, it guarantees that such monitors are automatically generated following a Correct-by-Construction (CbC) approach while also guaranteeing that their deployment in the SUS does not negatively influence either the functional or the non-functional safety/security aspects of the SUS.
To achieve that, MARS will feature a Domain Specific Language (DSL) tailored to ease the specification of monitors while also incorporating relevant details of the SUS platform. By combining information given by the system’s design team, MARS will apply a set of formal verification techniques that will guarantee that both monitor generation and monitor instrumentation in the SUS will comply with a set of safety and security properties. The compliance of such properties will be ensured by combining specifically created verification algorithms and external state-of-the-art (semi-)automatic formal verification tools like model checkers (e.g., mCRL2 and UPPAAL), SMT solvers, proof-assistants (e.g., Coq), and security-focused formal verifications tools (e.g., ProVerif).
In MARS, each physical computing unit is called a node. Developers may specify monitors targeting each node’s internal aspects or aim to verify the communication among nodes, assuming a distributed system. A specification example of a node in MARS is illustrated in Figure 1. There, the deployment platform’s characteristics, functionalities, and the time constraints of its tasks and modes of operation are specified. These specifications can be seen as contracts to be followed for the node’s implementation phase. On top of that, pre/post conditions can be specified for the automatic monitoring generation and user-provided monitor specification of the monitors themselves.
As previously mentioned, MARS’s context of application involves safety-critical systems. Such systems are commonly built on top of embedded systems, meaning they present strict performance and temporal constraints. Supported platforms range from single-board computers like the Raspberry Pi and the NVIDIA Jetson Nano to microcontrollers like the ESP32. To broaden the types of application where MARS could be useful, ROS2 and micro-ROS have been placed at the center of the development efforts given their flexibility in terms of applications while still maintaining a well-defined type of system architecture. Other similar distributed communication frameworks, such as MQTT and ZeroMQ, are also being considered due to their wide applicability in industrial contexts, notably, Industry 4.0.
References
[1] R. Rajkumar, I. Lee, L. Sha, and J. Stankovic. Cyber-physical systems: The next computing revolution. InDesign Automation Conference, pages731–736, June 2010
[2] Osepchuk, B. Safety-Critical Software: 15 things every developer should know. Small Business Programming. 2020, October 22 https://smallbusinessprogramming.com/safety-critical-software-15-things-every-developer-should-know
[3] Raju S., Rytarowski K. An introduction to Formal Verification for Software Systems. Moritz Systems. 2020, August 19. https://www.moritz.systems/blog/an-introduction-to-formal-verification/
[4] Bartocci E., Falcone Y., Francalanza A., and Reger G. Introduction to runtime verification. InLectures on Runtime Verification,pages 1–33. Springer International Publishing, 2018.
[5] G. S. Nandi, D. Pereira, J. Proença and E. Tovar, “Work-In-Progress: a DSL for the safe deployment of Runtime Monitors in Cyber-Physical Systems,” 2020 IEEE Real-Time Systems Symposium (RTSS), 2020, pp. 395-398, doi: 10.1109/RTSS49844.2020.00047.
Authors
Giann Spilere Nandi, research fellow at the CISTER Research Centre/ISEP.
Giann is a Ph.D. candidate of the Doctoral Program in Electrical and Computer Engineering of the Faculty of Engineering of the Universidade do Porto. His previous education includes a 5-year degree in Computer Engineer, issued by the Universidade Federal de Santa Catarina and a one-year exchange program, at the Hanzehogeschool Groningen, specializing in Electronic Product Design and Engineering. Since July 2018, Giann has been working in research activities in the domains of safety-critical systems, formal methods, and security, which are his main areas of interest.
David Pereira, integrated Researcher at CISTER Research Centre/ISEP
David is a member of the Board of Directors and Senior Researcher at CISTER/ISEP, as well as member of the Scientific Board of the Vortex collaborative laboratory on cyber-physical systems & cyber security, and Invited Professor at ISEP. He holds a PhD in Computer Science by the MAP-i PhD Programme, awarded in 2013 by the Universities of Minho, Aveiro and Porto He is the technical leader of CISTER’s participation in the VORTEX CoLAB, the PI of the REASSURE project on secure runtime verification of RTECS, technical co-leader of CISTER in flagship international projects including ENABLE-S3 and EMC2, and a technical contributor in other industry-driven projects.
José Proença, assistant researcher at the CISTER Research Centre/ISEP
José Proença is an assistant researcher and invited professor at Instituto Politécnico do Porto Instituto Superior de Engenharia do Porto, working in the Research Center in Real-Time & Embedded Computing Systems, investigating mainly coordination aspects and formal methods in the context of Cyber-Physical Systems. He is actively involved in a H2020 project and in 2 FCT projects, in one of which as coordinator. He currently belongs to the steering committee of 2 international conferences in fundamental computer science, he chaired the program committee of 5 international research venues with edited proceedings, edited 2 journal volumes, and was the member of 16 program-committees of international venues.
