nusmv是形式化验证的一个常用工具，主要可以进行LTL，CTL的建模。windows版。

nuXmv是一种新的符号模型检查器，用于分析同步有限状态和有限状态系统。 nuXmv扩展NuSMV沿着两个主要方向: 对于有限状态的情况，nuXmv具有基于最先进的基于SAT的算法的强大验证引擎。 对于无限状态的情况，nuXmv具有基于SMT的验证技术，通过与数学5。 查看的完整列表特征由nuXmv提供，或者看看用户手册。 nuXmv目前以二进制形式获得许可，用于非商业或学术目的。

这是一个描述三层楼中电梯运行情况的基于NuSMV的程序

In this tutorial we give a short introduction to the usage of the main functionalities of NUSMV. In Chapter 2 [Examples], page 3 we describe the input language of NUSMV by presenting some examples of NUSMV models. Chapter 3 [Simulation], page 8 shows how the user can get familiar with the behavior of a NUSMV model by exploring its possible executions. Chapter 4 [CTL Model Checking], page 13 and Chapter 5 [LTL Model Checking], page 17 give an overview of BDD-based model checking, while Chapter 6 [Bounded Model Checking], page 20 presents SAT-based model checking in NUSMV.

NuSMV-2.5.4-i386-pc-mingw32,下载后装到其他盘

定义为表格的模式转换可以轻松转换为 Matlab 和 NuSMV 代码，以便在 SDV 和 NuSMV 工具中使用。 这用于正式证明模式转换的正确性。 提供了两个示例 - 一个是较早的自动驾驶仪模式转换，另一个是通用表。

资源：一份源代码，一份英文报告。英文报告包括了模拟运行结果（20步随机），还有CTL以及CTL验证结果，最后一些简单说明。

基于NuSMV语言描述三层电梯的行为，并对相关性质进行模型检测。是一个模型检测应用的简单例子。