.png){kind=icon}
返回
FRET2WEST: Exploring translation between temporal logic representations
.png){kind=icon}
PRE
AI
DOI：10.5381/jot.2026.25.1.a2.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
软件需求通常以自然语言表达，若需用于形式化方法，则必须进行形式化处理，以便在执行过程中验证实现是否符合其需求。工具如形式化需求提取工具（FRET）支持此类需求形式化，并为每个需求生成线性时态逻辑（LTL）公式，这些公式可用于形式化验证，通常通过模型检测实现。本文探讨了与不同需求表示形式协同工作的工具集成。具体而言，我们关注将FRET的LTL输出翻译为任务时态LTL（MLTL）。这使FRET能够与WEST工具集成，该工具将MLTL公式转换为逻辑等价的正则表达式，描述所有满足的轨迹集合，从而便于通过运行时验证工具（如R2U2）验证规范。这种集成使WEST能够验证FRET生成的规范。我们的解决方案FRET2WEST利用基于正则表达式的映射、变量规范化以及任务时间间隔翻译，将FRET的LTL规范转换为WEST的MLTL语法。一个通过案例研究迭代构建的概念验证JavaScript翻译器，被添加为FRET工具的一个功能。
Keyword:
Safety-critical systems
Formal verification
Temporal logic
FRET
WEST
Toolchain interoperability
