通过结构化自然语言的形式化表述实现语义一致性：FRETish 案例研究

形式化是将系统需求以形式语言书写的过程，这些需求大多源自自然语言。在形式方法领域，形式化常被认为是验证过程中最细致且最复杂的步骤之一。不乏情况的是，形式化工具和环境选择 various levels of requirement descriptions：自然语言、技术语言、图表示和形式语言等。在文献中，有各种原则和准则旨�引导需求形式化过程。本文提出了一条新指南：通过形式化实现语义一致性。该指南指出，上述各种形式化层次应大致遵循相同的逻辑结构。这一原则在LLM被请求执行可由形式工具使用结构化自然语言检查的推理任务中尤为 relevant，其中结构化自然语言作为中间层桥接两种范式。在语义一致性的背景下，我们分析了NASA的形式需求收集工具FRET，并提出了将受控自然语言FRETish自动翻译为MTL形式语言的替代方案。我们比较了新的翻译与原始翻译，并通过模型检查证明等价性。进行了一些统计分析，这些结果似乎倾向于新的翻译。如预期，翻译过程产生了有趣的反思，揭示了一些我们将呈报告并讨论的不一致性。