NuSMV模型验证器实现分析

摘要

模型检测(Model Checking)是由E.M.Clarke与E.A.Emerson提出的一种形式化验证方法。其基本思想是在有限状态转移系统上，通过穷尽搜索的方法，验证系统规范是否得到满足。它广泛用于验证数字电路系统和网络协议系统的设计是否正确。模型检测的一个基本问题是状态爆炸问题，针对这个问题，已提出多种解决方法，其中，符号模型检测技术是一个经典的缓解状态爆炸问题的方法。
　　 NuSMV是一个经典的模型检测工具，它高效地实现了符号模型检测技术。NuSMV主要由意大利特兰托大学的A.Cimatti和M.Roveri所开发，它有很好的软件体系结构，易于定制和扩展。
　　 目前有关NuSMV如何实现符号模型检测技术的文献资料不多，这限制了NuSMV的应用、定制和扩展。本文主要工作就是分析和研究NuSMV的实现源码，给出NuSMV实现符号模型检测技术的方法和原理。通过分析NuSMV的整体体系结构、模块间的关系、模块内部的程序结构、模块间接口调用方法、内部数据结构和算法，获得了一份详细的分析文档。该分析文档给出了有限状态转移系统和规范用OBDD(有序二叉决策图)表示的具体方法、用OBDD实现模型检测算法的方法和NuSMV的实现代码与符号模型检测技术理论层面的对应关系。论文结合大量的实例检验和说明分析结果。本文的分析结果，对NuSMV进行定制和扩展具有参考价值。

目录

文摘

英文文摘

声明

第一章绪论

1.1研究背景

1.2模型检测工具

1.3主要工作

1.4论文组织

第二章模型检测

2.1 Kripke结构和时态逻辑

2.2模型检测算法

2.3符号模型检测技术

2.4本章小结

第三章NuSMV概述

3.1 NuSMV介绍及其功能

3.2 NuSMV编译、安装和使用

3.3 NuSMV输入语言

3.4本章小结

第四章NuSMV体系结构总结

4.1 NuSMV逻辑结构

4.2 NuSMV目录结构

4.3 NuSMV源码命名规范

4.4本章小结

第五章NuSMV核心模块分析

5.1 sm模块、cmd模块和utils模块

5.2 node模块和parser模块

5.3 dd模块

5.4 compile模块、enc模块和fsm模块

5.5 mc模块

5.6本章小结

第六章总结与展望

6.1主要工作总结

6.2进一步的工作

参考文献

致谢