skip to main content


Title: Towards a Model-Integrated Runtime Monitoring Infrastructure for Cyber-Physical Systems
Runtime monitoring is essential for ensuring the safe operation and enabling self-adaptive behavior of Cyber-Physical Systems (CPS). It requires the creation of system monitors, instrumentation for data collection, and the definition of constraints. All of these aspects need to evolve to accommodate changes in the system. However, most existing approaches lack support for the automated generation and setup of monitors and constraints for diverse technologies and do not provide adequate support for evolving the monitoring infrastructure. Without this support, constraints and monitors can become stale and become less effective in long-running, rapidly changing CPS. In this ``new and emerging results'' paper we propose a novel framework for model-integrated runtime monitoring. We combine model-driven techniques and runtime monitoring to automatically generate large parts of the monitoring framework and to reduce the maintenance effort necessary when parts of the monitored system change. We build a prototype and evaluate our approach against a system for controlling the flights of unmanned aerial vehicles.  more » « less
Award ID(s):
1931962 1741781
NSF-PAR ID:
10297239
Author(s) / Creator(s):
; ; ; ;
Date Published:
Journal Name:
International Conference on Software Engineering: New Ideas and Emerging Results
Volume:
2021
Page Range / eLocation ID:
96 to 100
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Fill, Hans-Georg ; Mayo, Francisco ; van Sinderen, Marten ; Maciaszek, Leszek (Ed.)
    Safety-critical real-time systems require correctness to be validated beyond the design phase. In these systems, response time is as critical as correct functionality. Runtime verification is a promising approach for validating the correctness of system behaviors during runtime using monitors derived from formal system specifications. However, practitioners often lack formal method backgrounds, and no standard notation exists to capture system properties that serve their needs. To encourage the adoption of formal methods in industry, we present GROOT, a runtime monitoring tool for real-time systems that automatically generates efficient monitors from structured English statements. GROOT is designed with two branches, one for functional requirements and one for specifications with metric time constraints, which use appropriate formalisms to synthesize monitors. This paper introduces TIMESPEC, a structured English dialect for specifying timing requirements. Our tool also automates formal analysis to certify the C monitors’ construction. We apply GROOT to timing specifications from an industrial component and a simulated autonomous system in Simulink. 
    more » « less
  2. Unmanned aerial vehicles (UAVs) are becoming increasingly pervasive in everyday life, supporting diverse use cases such as aerial photography, delivery of goods, or disaster reconnaissance and management. UAVs are cyber-physical systems (CPS): they integrate computation (embedded software and control systems) with physical components (the UAVs flying in the physical world). UAVs in particular and CPS in general require monitoring capabilities to detect and possibly mitigate erroneous and safety-critical behavior at runtime. Existing monitoring approaches mostly do not adequately address UAV CPS characteristics such as the high number of dynamically instantiated components, the tight integration of elements, and the massive amounts of data that need to be processed. In this paper we report results of a case study on monitoring in UAVs. We discuss CPS-specific monitoring challenges and present a prototype we implemented by extending REMINDS, a framework for software monitoring so far mainly used in the domain of metallurgical plants. Additionally, we demonstrate the applicability and scalability of our approach by monitoring a real control and management system for UAVs in simulations with up to 30 drones flying in an urban area. 
    more » « less
  3. Many Cyber-Physical Systems (CPS) have timing constraints that must be met by the cyber components (software and the network) to ensure safety. It is a tedious job to check if a CPS meets its timing requirement especially when they are distributed and the software and/or the underlying computing platforms are complex. Furthermore, the system design is brittle since a timing failure can still happen e.g., network failure, soft error bit flip, etc. In this paper, we propose a new design methodology called Plan B where timing constraints of the CPS are monitored at the runtime, and a proper backup routine is executed when a timing failure happens to ensure safety. We provide a model on how to express the desired timing behavior using a set of timing constructs in a C/C++ code and how to efficiently monitor them at the runtime. We showcase the effectiveness of our approach by conducting experiments on three case studies: 1) the full software stack for autonomous driving (Apollo), 2) a multi-agent system with 1/10th scale model robots, and 3) a quadrotor for search and rescue application. We show that the system remains safe and stable even when intentional faults are injected to cause a timing failure. We also demonstrate that the system can achieve graceful degradation when a less extreme timing failure happens. 
    more » « less
  4. Runtime verificationis a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronousdistributedmonitors observing the system, only if each monitor can emit verdicts taken from alarge enoughfinite set. We revisit this impossibility result in the concrete context of linear-time logic (ltl) semantics for runtime verification, that is, when the correctness of the system is specified by anltlformula on its execution traces. First, we show that monitors synthesized based on the 4-valued semantics ofltl(rv-ltl) may result in inconsistent distributed monitoring, even for some simpleltlformulas. More generally, given anyltlformula φ, we relate the number of different verdicts required by the monitors for consistently monitoring φ, with a specific structural characteristic of φ called itsalternation number. Specifically, we show that, for everyk ≥ 0, there is anltlformula φ with alternation number kthat cannot be verified at runtime by distributed monitors emitting verdicts from a set of cardinality smaller thank+ 1. On the positive side, we define a family of logics, calleddistributedltl(abbreviated asdltl), parameterized byk≥ 0, which refinesrv-ltlby incorporating2k+ 4 truth values. Our main contribution is to show that, for everyk≥ 0, everyltlformula φ with alternation number kcan be consistently monitored by distributed monitors, each running an automaton based on a (2 ⌈k/2 ⌉ +4)-valued logic taken from thedltlfamily.

     
    more » « less
  5. Denial of service (DoS) attacks increasingly exploit algorithmic, semantic, or implementation characteristics dormant in victim applications, often with minimal attacker resources. Practical and efficient detection of these asymmetric DoS attacks requires us to (i) catch offending requests in-flight, before they consume a critical amount of resources, (ii) remain agnostic to the application internals, such as the programming language or runtime system, and (iii) introduce low overhead in terms of both performance and programmer effort. This paper introduces FINELAME, a language-independent framework for detecting asymmetric DoS attacks. FINELAME leverages operating system visibility across the entire software stack to instrument key resource allocation and negotiation points. It leverages recent advances in the Linux extended Berkeley Packet Filter virtual machine to attach application-level interposition probes to key request processing functions, and lightweight resource monitors--user/kernel-level probes--to key resource allocation functions. The data collected is used to train a model of resource utilization that occurs throughout the lifetime of individual requests. The model parameters are then shared with the resource monitors, which use them to catch offending requests in-flight, inline with resource allocation. We demonstrate that FINELAME can be integrated with legacy applications with minimal effort, and that it is able to detect resource abuse attacks much earlier than their intended completion time while posing low performance overheads. 
    more » « less