Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards A Catalogue of Requirement Patterns for Space Robotic Missions

Mahdi Etumi, Hazel M. Taylor, Marie Farrell

TL;DR

This work investigates whether existing robotic specification patterns can support autonomous space missions and introduces five new space-domain patterns. By assembling a corpus of 116 formally captured space mission requirements and formalising them in LTL and FRETish, the authors demonstrate that while existing patterns are broadly applicable, additional patterns and variants are needed to cover space-specific behaviors. An expert evaluation provides insights into the utility and limitations of the new patterns, highlighting opportunities for probabilistic, real-time, and first-order extensions to FRETish. The study offers a practical baseline for applying formal methods to space missions and points to future work in pattern composition, broader domain coverage, and large-scale validation across agencies and missions.

Abstract

In the development of safety and mission-critical systems, including autonomous space robotic missions, complex behaviour is captured during the requirements elicitation phase. Requirements are typically expressed using natural language which is ambiguous and not amenable to formal verification methods that can provide robust guarantees of system behaviour. To support the definition of formal requirements, specification patterns provide reusable, logic-based templates. A suite of robotic specification patterns, along with their formalisation in NASA's Formal Requirements Elicitation Tool (FRET) already exists. These pre-existing requirement patterns are domain agnostic and, in this paper we explore their applicability for space missions. To achieve this we carried out a literature review of existing space missions and formalised their requirements using FRET, contributing a corpus of space mission requirements. We categorised these requirements using pre-existing specification patterns which demonstrated their applicability in space missions. However, not all of the requirements that we formalised corresponded to an existing pattern so we have contributed 5 new requirement specification patterns as well as several variants of the existing and new patterns. We also conducted an expert evaluation of the new patterns, highlighting their benefits and limitations.

Towards A Catalogue of Requirement Patterns for Space Robotic Missions

TL;DR

This work investigates whether existing robotic specification patterns can support autonomous space missions and introduces five new space-domain patterns. By assembling a corpus of 116 formally captured space mission requirements and formalising them in LTL and FRETish, the authors demonstrate that while existing patterns are broadly applicable, additional patterns and variants are needed to cover space-specific behaviors. An expert evaluation provides insights into the utility and limitations of the new patterns, highlighting opportunities for probabilistic, real-time, and first-order extensions to FRETish. The study offers a practical baseline for applying formal methods to space missions and points to future work in pattern composition, broader domain coverage, and large-scale validation across agencies and missions.

Abstract

In the development of safety and mission-critical systems, including autonomous space robotic missions, complex behaviour is captured during the requirements elicitation phase. Requirements are typically expressed using natural language which is ambiguous and not amenable to formal verification methods that can provide robust guarantees of system behaviour. To support the definition of formal requirements, specification patterns provide reusable, logic-based templates. A suite of robotic specification patterns, along with their formalisation in NASA's Formal Requirements Elicitation Tool (FRET) already exists. These pre-existing requirement patterns are domain agnostic and, in this paper we explore their applicability for space missions. To achieve this we carried out a literature review of existing space missions and formalised their requirements using FRET, contributing a corpus of space mission requirements. We categorised these requirements using pre-existing specification patterns which demonstrated their applicability in space missions. However, not all of the requirements that we formalised corresponded to an existing pattern so we have contributed 5 new requirement specification patterns as well as several variants of the existing and new patterns. We also conducted an expert evaluation of the new patterns, highlighting their benefits and limitations.

Paper Structure

This paper contains 12 sections, 2 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Methodology
  4. Requirement Specification Patterns
  5. Description of Space Missions Surveyed
  6. New Patterns with LTL and FRET Formalisation
  7. Requirement Pattern Metrics and Analysis
  8. Expert Evaluation
  9. Discussion: Answering the Research Questions
  10. Conclusion and Future Work
  11. Acknowledgements:
  12. Table of Requirements

Figures (2)

  • Figure 1: The space missions that are described in Section \ref{['subsec:missionoverview']}. These images are taken from the surveyed literature, NASA, ESA and JAXA sources.
  • Figure 2: Robotic mission patterns, those with a white/grey background were proposed in Menghi2019SpecPatternsRoboticMissions, those with a yellow background were proposed in Vazquez2024RoboticMissionFRET and our new patterns are shown with an orange background.