SpecForge – A Platform for Authoring Formal Specifications
17 hours ago
- SpecForge 是一款使用Lilo语言编写和分析时序规范的工具，支持基本类型、算术、逻辑以及像always、eventually、past、historically这样的时序运算符，并可设定时间区间。
- Lilo规范按系统组织，包含信号、参数、类型、定义和规约；一个温度控制系统示例说明了温度和湿度的安全需求。
- VSCode扩展为编写Lilo代码提供语法高亮、类型检查、警告以及规范可满足性支持。
- 分析功能包括：监控（对照规范检查迹）、示例（生成示例迹）、反例查找（借助模型搜索反例）、导出（将规范转换为JSON等格式）以及动画（可视化随时间变化的行为）。
- 监控功能评估记录迹数据是否符合规范，以树形结构显示子表达式结果及解释；分析结果可保存并重新打开。
- 示例功能通过生成满足规范的迹，帮助理解有效行为并测试组件，辅助规范编写。
- 反例查找需要注册反例查找脚本和模型；结果通过监控树展示模型违规情况。
- 导出功能将规范转换为其他格式以供其他工具使用，例如JSON。