为航天机器人任务提炼可复用的规范模式,提升需求形式化表达能力。
Towards A Catalogue of Requirement Patterns for Space Robotic Missions
- 基于现有模式库,将航天任务需求映射到逻辑模板中。
- 从文献分析中提取20+条真实需求,验证并扩展模式库。
- 提出5个新需求模式,适合航天系统形式化设计人员使用。
在安全与任务关键型系统(如自主航天机器人任务)开发中,复杂行为常在需求获取阶段被捕捉。由于需求多以自然语言表达,存在歧义且难以进行形式化验证。为支持形式化需求定义,规范模式提供可复用的逻辑模板。已有针对机器人的规范模式及在NASA FRET工具中的形式化实现。本文通过文献回顾分析多个航天任务,利用FRET形式化其需求,构建了航天任务需求语料库。通过预设模式对这些需求进行分类,验证了现有模式在航天场景的适用性。但部分需求无法匹配现有模式,因此新增5个需求规范模式,并提出若干变体。同时对新模式进行专家评估,揭示其优势与局限。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。