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.

翻译：在开发安全关键与任务关键系统（包括自主空间机器人任务）时，复杂行为通常在需求获取阶段被捕获。需求通常使用自然语言表达，这种方式存在歧义且难以适用于能够提供系统行为稳健保证的形式化验证方法。为支持形式化需求的定义，规约模式提供了可复用的、基于逻辑的模板。一套机器人规约模式及其在美国国家航空航天局（NASA）形式化需求获取工具（FRET）中的形式化表达已经存在。这些现有需求模式是领域无关的，本文探讨了它们在空间任务中的适用性。为此，我们对现有空间任务进行了文献综述，并使用FRET对其需求进行了形式化，贡献了一个空间任务需求语料库。我们使用现有规约模式对这些需求进行了分类，证明了它们在空间任务中的适用性。然而，并非所有我们形式化的需求都能与现有模式对应，因此我们贡献了5个新的需求规约模式，以及若干现有模式和新模式的变体。我们还对新模式进行了专家评估，突出了其优势与局限性。