SafeNL 安全需求验证

领域专家免依赖形式专家

通过将自然语言需求转换为 SafeNL 模式并自动转换为形式模型，领域专家可独立完成一致性验证，无需与形式专家反复沟通。

陈小红 · Juan, Zhang · Jin Z. · 张敏 · 李童 · Chen, Xiang · Zhou, Tingliang

IEEE Transactions on Intelligent Transportation Systems 2023

参数信息

验证时间减少百分比

90 %

技术优势

时间节省至少九成

无需等待形式专家响应，沟通成本大幅降低。

不懂形式方法也能用

领域专家只需将需求写成 SafeNL 模式，工具自动转换为形式模型并完成验证。

自动定位问题需求

发现不一致后能定位到具体需求，减少排查时间。

应用场景

• 安全苛求系统：用于高效验证安全需求一致性，降低对形式专家依赖。
• 铁路信号：将铁路信号安全需求转为 SafeNL 模式，快速检查一致性并定位问题。
• 需求工程：提供模式化语言和工具支持，简化需求形式化与验证流程。