Real-time Mode-Aware Dataflow: A Dataflow Model to Specify and Analyze Mode-dependent CPSs under Relaxed Timing Constraints

TL;DR

This work addresses the challenge of analyzing cyber-physical systems that exhibit both mode-dependent execution and relaxed real-time constraints. It introduces Real-time Mode-aware Dataflow (RMDF), an extension of PolyGraph that adds routing and mode deciders to capture conditional execution branches while preserving PolyGraph's static timing analyses. The key contributions include extending consistency and liveness analyses, adapting timing analysis, and proposing a feasibility test, demonstrated on the Ingenuity Mars helicopter vision system. The RMDF framework enables rigorous, scalable timing analysis for complex mode-switching CPS and provides a path toward applying these concepts to other design tools and real-world systems.

Abstract

Modern Cyber-Physical Systems (CPS) often exhibit both relaxed real-time constraints and a mode-dependent execution. Relaxed real-time constraints mean that only a subset of the processes of a CPS have real-time constraints, and a mode-dependent CPS has conditional execution branches. Static analysis tools, such as the PolyGraph model (a formalism extending the Cyclo-Static Dataflow model with real-time constraints), can specify and analyze systems with relaxed real-time constraints. However, PolyGraph is limited in its ability to specify and analyze mode-dependent CPSs. This paper extends PolyGraph with routing actors, yielding the Routed PolyGraph model. This model is further extended to the Real-time Mode-Aware Dataflow (RMDF), which both leverages routing actors and incorporates a new dataflow actor to specify mode-dependent CPSs under relaxed real-time constraints. This paper also extends the static analyses of PolyGraph to RMDF. We showcase the application of RMDF with a specification and an analysis (derivation of timing constraints at the job-level and a feasibility test) of the vision processing system of the Ingenuity Mars helicopter.

Figures (9)

• Figure 1: An illustration of a disjoint directed mesh with three branches. $n_1$ to $n_3$ are the (bounded positive) number of actors in each branch.
• Figure 2: Illustration of a splitter, a joiner, a duplicater, and a discard with their input and output traces. Rates of $1$ and initial tokens of $0$ are omitted for clarity.
• Figure 3: Removal of routing actors while preserving the semantics of data communication pattern. Rates of $1$ and initial tokens of $0$ are omitted for clarity.
• Figure 4: An illustration of a controlled splitter and a controlled joiner with their input and output traces. Dashed lines represent control channels, and plain lines represent data channels. Rates of $1$ and initial tokens of $0$ are omitted for clarity.
• Figure 5: An example of an RMDF specification. A usual actor is an actor which is neither (non-) controlled splitter or joiner, nor a mode decider.

Theorems & Definitions (9)

• Definition 1: Floor and ceil functions
• Definition 2: Control area of a mode decider
• Definition 3: Mode-coherent RMDF specification
• Theorem 1: Consistent and live RMDF specification
• proof : Proof of \ref{['theorem-1']}
• Definition 4: Well-defined PolyGraph/RMDF specification
• Theorem 2: Derivation of the execution windows of a PolyGraph specification - Theorem 1 of roumage_static_2024
• Theorem 3: Derivation of the execution windows of an RMDF specification
• proof : Proof of \ref{['thm:execution-windows-rmdf']}