面向太空机器人任务的需求模式目录构建

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