Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Ingenuity Mars Helicopter Specified and Analyzed with the Real-time Mode-aware Dataflow Model

Guillaume Roumage, Selma Azaiez, Cyril Faure, Stéphane Louise

TL;DR

This work addresses safety-critical timing guarantees for an autonomous Mars CPS by modeling Ingenuity with Real-time Mode-aware Dataflow (RMDF). It develops an RMDF specification for Ingenuity's vision, navigation, and control subsystems, and uses static analyses to establish consistency and liveness while deriving timing behavior and performing a feasibility test. The results include a detailed, mode-aware dataflow model, timing windows for each actor, and a plausible RMDF-based explanation for the sixth-flight anomaly, along with fidelity notes on simplifying assumptions. The approach provides a rigorous foundation for preflight verification and informs potential runtime monitoring to enhance reliability in planetary robotics.

Abstract

Ingenuity is an autonomous Cyber-Pysical System (CPS) that has successfully completed more than 70 flights over Mars between 2021 and 2024. Ensuring the safety of its mission is paramount, as any failure could result in catastrophic economic damage and significant financial losses. Dataflow Models of Computation and Communication (DF MoCCs) serve as a formal framework for specifying and analyzing the timing behavior of such CPSs. In particular, the Real-time Mode-aware Dataflow (RMDF) model is highly suitable to specify and analyze real-time and mode-dependent Cyber-Physical Systems (CPSs) like Ingenuity. This paper showcases the application of RMDF for the specification and analysis of Ingenuity. We propose a dataflow specification of Ingenuity, analyze its timing behavior, and provide a feasibility test. Finally, we proposed a plausible explanation of the timing anomaly that occurred during the sixth flight of Ingenuity.

The Ingenuity Mars Helicopter Specified and Analyzed with the Real-time Mode-aware Dataflow Model

TL;DR

This work addresses safety-critical timing guarantees for an autonomous Mars CPS by modeling Ingenuity with Real-time Mode-aware Dataflow (RMDF). It develops an RMDF specification for Ingenuity's vision, navigation, and control subsystems, and uses static analyses to establish consistency and liveness while deriving timing behavior and performing a feasibility test. The results include a detailed, mode-aware dataflow model, timing windows for each actor, and a plausible RMDF-based explanation for the sixth-flight anomaly, along with fidelity notes on simplifying assumptions. The approach provides a rigorous foundation for preflight verification and informs potential runtime monitoring to enhance reliability in planetary robotics.

Abstract

Ingenuity is an autonomous Cyber-Pysical System (CPS) that has successfully completed more than 70 flights over Mars between 2021 and 2024. Ensuring the safety of its mission is paramount, as any failure could result in catastrophic economic damage and significant financial losses. Dataflow Models of Computation and Communication (DF MoCCs) serve as a formal framework for specifying and analyzing the timing behavior of such CPSs. In particular, the Real-time Mode-aware Dataflow (RMDF) model is highly suitable to specify and analyze real-time and mode-dependent Cyber-Physical Systems (CPSs) like Ingenuity. This paper showcases the application of RMDF for the specification and analysis of Ingenuity. We propose a dataflow specification of Ingenuity, analyze its timing behavior, and provide a feasibility test. Finally, we proposed a plausible explanation of the timing anomaly that occurred during the sixth flight of Ingenuity.
Paper Structure (29 sections, 4 figures, 3 tables)

This paper contains 29 sections, 4 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Contribution
  3. Paper Organization
  4. Background and Terminology
  5. The SDF Model
  6. The PolyGraph Model
  7. Syntax and Semantic
  8. Rational production and consumption rates
  9. Timing constraints
  10. The RMDF model
  11. Mode-Dependent Execution
  12. Splitters and Joiners
  13. Mode Deciders, Controlled Splitters and Control Joiners
  14. Control areas
  15. The Ingenuity Mars Helicopter
  16. ...and 14 more sections

Figures (4)

  • Figure 1: An example of an RMDF specification. A usual actor is an actor which is neither (non-) controlled splitter or joiner, nor a mode decider.
  • Figure 2: An overview of the Ingenuity helicopter.
  • Figure 3: An RMDF specification of Ingenuity deployed after its sixth flight and the specification of its channel characteristics.
  • Figure 4: Schedule of the actors of the vision processing leading to the anomaly of its sixth flight.