名称: 模型检查器接口 描述: 与多种形式化验证模型检查工具交互 允许使用的工具:
- Bash
- 读取
- 写入
- 编辑
- 全局匹配
- 文本搜索 元数据: 专业领域: 计算机科学 领域: 科学 类别: 形式化验证 阶段: 6
模型检查器接口
目的
为系统和协议的形式化验证提供使用模型检查工具的专家指导。
功能
- SPIN/Promela 规范生成
- NuSMV/NuXMV 接口
- 用于时序系统的 UPPAAL
- 结果解析与可视化
- 反例追踪分析
- 抽象精化
使用指南
- 工具选择: 选择合适的模型检查器
- 规范编写: 将系统转换为检查器的语言
- 属性定义: 指定要验证的属性
- 检查执行: 运行模型检查器
- 结果分析: 解释结果和反例
工具/库
- SPIN
- NuSMV
- UPPAAL
- PRISM