nuXmv模型检测实战：从交通灯控制器实例掌握形式化验证

1. 项目概述从理论到实践的模型检测之旅最近在梳理形式化验证相关的知识体系发现很多朋友对nuXmv这个工具既好奇又有点发怵。好奇是因为它在学术界和工业界尤其是硬件、协议验证领域的名气确实响亮发怵则是因为它的学习曲线相对陡峭官方文档虽然详尽但更像一本参考手册缺少那种“手把手带你跑通第一个例子”的亲切感。我自己也是从一堆抽象的时序逻辑公式和状态机概念里摸爬滚打过来的深知第一个能跑起来、能看出结果的实例有多重要。它就像一把钥匙能帮你打开理解模型检测这扇大门。所以这篇笔记的核心目标非常直接抛开复杂的理论推导聚焦于一个完整的、可复现的nuXmv模型检测实例。我们将一起构建一个简单的系统模型用nuXmv的输入语言一种类SMV的语言来描述它然后提出我们关心的性质用CTL或LTL公式表达最后命令nuXmv去自动验证这些性质是否成立。整个过程我会把重点放在“怎么做”和“为什么这么做”上比如语法为什么这样写、命令参数怎么选、输出结果怎么看懂。你会发现一旦跨过最初的语法门槛模型检测带来的那种“机器自动穷尽搜索所有可能状态并给出确定结论”的爽快感是其他测试方法难以比拟的。无论你是学生、研究员还是对高可靠性系统设计感兴趣的工程师这个实例都能为你提供一个坚实的起点。2. 实例背景一个简单的交通灯控制器为了把概念讲清楚我们选择一个足够小但又包含了并发、状态和时序特性的经典例子一个十字路口的交通灯控制器。这个例子在形式化方法教材里很常见因为它贴近生活状态空间有限非常适合教学。我们的简化系统如下场景一个双向比如南北向和东西向通行的十字路口。组件两盏灯分别控制两个方向。每盏灯都有三种状态红(Red)、黄(Yellow)、绿(Green)。安全规则任何时候两个方向的灯不能同时为绿色防止撞车。任何一盏灯从绿变红之前必须先经过黄灯状态提供缓冲时间。灯的状态按固定周期循环绿 - 黄 - 红 - 绿 ...系统行为两个方向的灯独立按周期运行但它们的状态组合必须始终遵守上述安全规则。我们要做的就是将这个用自然语言描述的系统转化为nuXmv能理解的精确数学模型然后验证它是否永远满足我们定义的安全规则。这就是模型检测的典型工作流建模 - 规约定义性质 - 验证。2.1 为什么选择nuXmv来做这件事你可能会问为什么不用编程语言模拟nuXmv的优势在于穷尽性验证对于有限状态系统nuXmv会探索所有可能的状态和状态转移序列。模拟测试只能覆盖有限的路径而模型检测理论上能证明性质在所有情况下都成立或找到一个反例。形式化规约性质用CTL/LTL等时序逻辑公式描述其语义是数学上精确的没有自然语言的二义性。比如“最终”和“一直”在逻辑公式里有严格定义。自动化与反例生成如果性质被违反nuXmv会自动生成一条最简的反例路径从初始状态一步步展示到出错状态。这对于调试和理解系统缺陷至关重要比单纯的“测试失败”信息量大多了。3. 模型构建用SMV语言描述交通灯系统现在我们开始动手编写nuXmv的模型文件通常保存为.smv后缀。我会逐模块解释你可以跟着一起写。3.1 模块定义与状态变量首先我们定义一个主要的模块main。MODULE main VAR light_ns : {green, yellow, red}; -- 南北向灯 light_ew : {green, yellow, red}; -- 东西向灯MODULE main: 每个nuXmv模型都有一个主模块。VAR: 用于声明变量。这里我们声明了两个变量light_ns和light_ew。{green, yellow, red}: 定义了变量的枚举类型。每个灯的状态只能取这三个值中的一个。这是一种非常直观的定义状态空间的方式。3.2 定义状态转移关系系统的动态行为这是模型的核心部分定义了系统如何从一个状态演化到下一个状态。我们使用ASSIGN块和next()函数。ASSIGN init(light_ns) : red; init(light_ew) : green; next(light_ns) : case light_ns green : yellow; light_ns yellow : red; light_ns red : green; TRUE : light_ns; -- 默认情况保持原状实际上前三种情况已覆盖所有可能 esac; next(light_ew) : case light_ew green : yellow; light_ew yellow : red; light_ew red : green; TRUE : light_ew; esac;init(): 指定变量的初始值。这里我们让南北向灯初始为红东西向灯初始为绿。这是一个合法的初始状态没有双绿。next(): 指定变量在下一个时间步下一次状态转移的值。case...esac: 一个多路选择语句类似于编程中的switch-case。它根据变量当前的值决定其下一个值。转移逻辑描述的就是“绿-黄-红-绿”的循环。例如light_ns green : yellow;表示如果当前南北灯是绿色那么下一刻它就变为黄色。注意这里的case语句必须覆盖所有可能的当前值否则模型会不完整。我们用了TRUE : light_ns;作为默认分支这是一个好习惯虽然本例中枚举值已被前面分支覆盖。3.3 添加系统不变性约束安全规则上面的模型只定义了每个灯自身的循环但没有强制两个灯之间的关系。我们需要添加约束让模型只允许符合安全规则的状态转移。这可以通过在TRANS、INVAR或ASSIGN的next()中增加条件来实现。这里我们选择在ASSIGN的case语句中加入约束使其更贴近“控制器决策”的逻辑。让我们修改next(light_ns)和next(light_ew)加入安全规则ASSIGN init(light_ns) : red; init(light_ew) : green; next(light_ns) : case -- 南北灯当前是绿色并且东西灯不是红色不这个约束不对。 -- 我们应该约束的是“下一个状态”不能出现双绿。 (light_ns green) (light_ew ! red) : yellow; -- 这是一个有问题的设计仅作演示 light_ns green : yellow; light_ns yellow : red; light_ns red : {green, red}; -- 尝试从红变绿时需要检查对方是否为红 TRUE : light_ns; esac;等一下这样直接把约束混在转移逻辑里会让case语句变得复杂且容易出错。更清晰、更模块化的做法是使用INVAR不变式来定义状态必须始终满足的条件以及TRANS来定义转移必须满足的条件。让我们重构一下采用更优雅的方式MODULE main VAR light_ns : {green, yellow, red}; light_ew : {green, yellow, red}; ASSIGN init(light_ns) : red; init(light_ew) : green; -- 每个灯独立的循环转移逻辑无约束的原始行为 next(light_ns) : case light_ns green : yellow; light_ns yellow : red; light_ns red : green; TRUE : light_ns; esac; next(light_ew) : case light_ew green : yellow; light_ew yellow : red; light_ew red : green; TRUE : light_ew; esac; -- 系统必须始终满足的不变性安全属性 INVAR !(light_ns green light_ew green) -- 规则1永远不能双绿 -- 状态转移必须满足的约束时序安全属性 TRANS -- 规则2从绿变红必须经过黄已经由循环逻辑保证这里可以显式声明 ( (light_ns green - next(light_ns) yellow) (light_ew green - next(light_ew) yellow) ) -- 规则3从红变绿时必须确保对方是红更强的互斥约束 ( (light_ns red next(light_ns) green) - (light_ew red) ) ( (light_ew red next(light_ew) green) - (light_ns red) )INVAR: 定义不变式。系统在任何可达状态下这个条件都必须为真。这里我们定义了规则1两个灯不能同时为绿。!表示逻辑非表示逻辑与。TRANS: 定义转移关系的全局约束。它规定了所有可能的状态转移必须满足的条件。这里我们定义了第一部分任何灯当前是绿下一刻必须是黄。这其实已经隐含在我们的case语句里但用TRANS显式写出可以作为双重检查。第二、三部分一个灯要从红变为绿前提是对方向的灯必须是红色。这是一个比“不能双绿”更强的约束它直接禁止了导致双绿状态出现的转移。实操心得在建模时将系统的“固有行为”ASSIGN中的next和“安全约束”INVAR,TRANS分开定义是很好的实践。这样模型更清晰也更容易调试。INVAR描述的是“状态空间的样子”TRANS描述的是“状态之间如何走动”。ASSIGN中的next可以看作是具体的“操作指南”而TRANS是必须遵守的“交通法规”。4. 性质规约用CTL公式表达我们要验证什么模型建好了接下来要告诉nuXmv我们想验证什么性质。这些性质用计算树逻辑CTL或线性时序逻辑LTL公式书写。我们先验证最基本的安全属性。在模型文件末尾MODULE main的所有定义之后我们添加SPEC语句。-- 性质规约 SPEC AG !(light_ns green light_ew green) -- 性质1全局永远无双绿 SPEC AG ((light_ns green) - AX (light_ns yellow)) -- 性质2南北绿后下一时刻必为黄 SPEC AG ((light_ew green) - AX (light_ew yellow)) -- 性质3东西绿后下一时刻必为黄 -- 性质4最终南北向灯总会变绿活性属性 SPEC AF (light_ns green) -- 性质5最终东西向灯总会变绿活性属性 SPEC AF (light_ew green)SPEC: 关键字后面跟着一个时序逻辑公式。AG p: CTL公式表示All pathsGlobally。意思是“在所有可能的未来路径上性质p一直为真”。这是非常强的不变性断言。我们的性质1和它上面的INVAR声明是等价的这里用SPEC来验证它是否真的在所有可达状态下成立。p - q: 逻辑蕴含如果p为真则q必须为真。AX p: CTL公式表示All pathsX(next)。意思是“在所有可能的未来路径上下一个时刻p为真”。性质2和3用这个来表达“绿灯后必是黄灯”的严格时序关系。AF p: CTL公式表示All pathsFuture。意思是“在所有可能的未来路径上最终在未来某个时刻p会为真”。这用来验证活性liveness即“好的事情最终会发生”比如每个方向的灯最终都能等到绿灯。5. 运行验证与结果解读保存文件为traffic_light.smv。现在我们启动nuXmv交互环境进行验证。5.1 启动与加载模型nuXmv -int traffic_light.smv-int参数表示进入交互模式。加载成功后你会看到nuXmv 提示符。5.2 执行模型检测在提示符后输入go check_propertygo: 命令nuXmv编译并构建模型的内部表示BDD或SAT编码。check_property: 执行对所有SPEC定义的性质的验证。5.3 分析输出结果nuXmv会依次输出每个性质SPEC的验证结果。对于我们的模型输出可能类似于-- specification AG !(light_ns green light_ew green) is true -- specification AG (light_ns green - AX light_ns yellow) is true -- specification AG (light_ew green - AX light_ew yellow) is true -- specification AF light_ns green is false -- specification AF light_ew green is falsetrue: 表示该性质在模型的所有可能行为下都成立。我们的前三个安全性质都通过了验证这很棒说明我们的模型遵守了基本的安全规则。false: 表示该性质被违反。我们的两个活性性质AF失败了这是一个非常重要的发现。5.4 深入排查为什么活性性质失败当性质为false时nuXmv会在交互模式下自动生成一个反例counterexample。我们需要查看这个反例来理解问题所在。在check_property之后我们可以用以下命令查看最后一个反例的轨迹show_traces -v -p 1-v: 详细模式显示所有变量的值。-p 1: 显示第1条轨迹通常就是刚生成的反例。输出会是一个状态序列例如Trace Description: Counterexample Trace Type: Counterexample - State 1.1 - light_ns red light_ew green - State 1.2 - light_ns green light_ew yellow - State 1.3 - light_ns yellow light_ew red - State 1.4 - light_ns red light_ew green -- Loop starts here - State 1.5 - light_ns green light_ew yellow ...仔细看这个轨迹状态在1.1、1.2、1.3、1.4之间循环然后回到1.1不看变量值1.4的状态是(red, green)而1.1也是(red, green)。实际上这个轨迹展示了一个循环(red, green) - (green, yellow) - (yellow, red) - (red, green) - ...。在这个循环里light_ns南北灯的状态序列是红 - 绿 - 黄 - 红 - 绿 ...。等等light_ns不是变成绿了吗是的在状态1.2它变成了绿。那么AF (light_ns green)应该为真啊为什么报告假这里有一个关键理解点AF p要求在所有路径上最终都满足p。我们的模型存在一条路径吗让我们检查TRANS约束。我们有一条约束(light_ns red next(light_ns) green) - (light_ew red)。在状态1.1light_nsred,light_ewgreen。根据这条约束light_ns不能从红变为绿因为light_ew不是红。那么状态1.2中的light_nsgreen是怎么来的矛盾了。这说明我们的模型有矛盾ASSIGN中的无条件循环逻辑 (red - green) 和TRANS中的强约束 (从红变绿要求对方为红) 冲突了。在状态1.1ASSIGN想让light_ns变绿但TRANS禁止这个转移。在nuXmv中当ASSIGN和TRANS冲突时TRANS具有更高的优先级它会限制ASSIGN定义的可能转移。实际上在状态1.1next(light_ns)唯一允许的值是red保持因为变成绿会违反TRANS。那么反例轨迹中的light_nsgreen是怎么出现的我犯了一个建模错误。在最初的、未加强TRANS约束的模型里活性性质可能就是真的。但当我添加了强互斥TRANS后我没有相应地修改ASSIGN中的next逻辑导致ASSIGN给出的“下一个值”可能不满足TRANS。在nuXmv语义中这并不会导致错误而是意味着从某些状态出发没有合法的下一个状态即系统“死锁”了。对于死锁状态AX p被定义为真因为不存在“下一个状态”所以“所有下一个状态都满足p”空洞地为真。但这会严重影响活性。更准确的建模方式是ASSIGN中的next应该只给出可能的、候选的下一个值而TRANS则过滤掉非法的转移。或者更简单直接地把所有约束都整合到ASSIGN的case语句里。让我们修复模型采用后一种更直观的方式。6. 模型修正与最终验证我们回到最初的想法将安全规则直接编码到状态转移逻辑中移除可能产生冲突的全局TRANS。修正后的模型 (traffic_light_fixed.smv):MODULE main VAR light_ns : {green, yellow, red}; light_ew : {green, yellow, red}; ASSIGN init(light_ns) : red; init(light_ew) : green; next(light_ns) : case light_ns green : yellow; -- 绿必变黄 light_ns yellow : red; -- 黄必变红 light_ns red : -- 红变绿的条件 case light_ew red : green; -- 只有对方是红自己才能变绿 TRUE : red; -- 否则保持红色 esac; TRUE : light_ns; esac; next(light_ew) : case light_ew green : yellow; light_ew yellow : red; light_ew red : case light_ns red : green; TRUE : red; esac; TRUE : light_ew; esac; -- 不变式永远不能双绿现在应该由转移逻辑保证了 INVAR !(light_ns green light_ew green) -- 性质规约 SPEC AG !(light_ns green light_ew green) -- 安全性质1 SPEC AG ((light_ns green) - AX (light_ns yellow)) -- 安全性质2 SPEC AG ((light_ew green) - AX (light_ew yellow)) -- 安全性质3 SPEC AF (light_ns green) -- 活性性质1 SPEC AF (light_ew green) -- 活性性质2 -- 新增互斥性一个绿则另一个必为红更强的表述 SPEC AG ((light_ns green) - (light_ew red)) SPEC AG ((light_ew green) - (light_ns red))主要修改在next(light_ns)和next(light_ew)中关于red - green的转移上我们嵌套了一个case语句只有在对向灯是红色时自己才能从红变绿否则就保持红色。这完美编码了互斥规则。现在重新用nuXmv加载并验证这个修正后的模型reset read_model -i traffic_light_fixed.smv go check_property预期输出将是所有SPEC的验证结果都为true。这证明我们的模型现在既安全无冲突又活性充足每个方向最终都能获得绿灯。7. 常见问题与排查技巧实录在实际使用nuXmv建模和验证时你肯定会遇到各种报错和意外结果。下面是我踩过的一些坑和总结的技巧。7.1 模型死锁与无初始状态现象执行go命令时提示No initial state exists或The model is deadlock-free? false。原因init()赋值矛盾。例如init(x) : 0;但INVAR x 0;。TRANS约束过强或者ASSIGN中next的值域与TRANS冲突导致从初始状态出发没有任何合法的下一状态死锁。变量定义的类型或范围有误。排查首先检查init语句确保初始值满足所有INVAR。使用print_current_state命令查看nuXmv认为的初始状态是什么。暂时注释掉TRANS和复杂的INVAR让模型先跑起来再逐一添加约束定位冲突源。使用check_fsm命令可以检查模型是否存在死锁状态。7.2 性质验证结果为“假”但找不到明显错误现象SPEC报告false但反例轨迹看起来符合预期或者自己觉得性质应该成立。原因对CTL/LTL算子的理解有误这是最常见的原因。比如混淆了AF p(最终总会p) 和AG p(一直p)或者混淆了A(所有路径) 和E(存在路径)。模型存在非预期的路径你的模型可能比你想的更具“非确定性”允许了更多行为其中一条路径违反了性质。性质公式写错了逻辑连接词 (,|,-,!) 的优先级或括号使用错误。排查仔细阅读反例轨迹show_traces -v是最好用的调试工具。一步一步看状态变化思考为什么在这条路径上性质不成立。简化性质如果验证AG (p - q)为假可以分别验证AG p和AG q是否成立或者用simulate命令随机模拟几条轨迹观察p和q的值。使用更简单的公式测试先验证一些显然成立的基本性质比如AG (light_ns red | light_ns yellow | light_ns green)状态值有效确保模型基础没问题。7.3 状态空间爆炸与验证性能现象对于稍复杂的模型go或check_property命令执行非常慢甚至内存耗尽。原因模型检测需要遍历所有可能的状态。状态数量随变量数量呈指数级增长状态空间爆炸。缓解策略抽象与简化这是最根本的方法。思考是否所有变量和细节都是验证当前性质所必需的能否合并一些状态能否用更小的数据类型如0..3代替0..255使用有界模型检测 (BMC)对于寻找反例bug特别有效。命令是check_ltlspec_bmc或check_ctlspec_bmc。它只探索一定深度-k参数指定内的状态而不是全部。如果在这个深度内找到了反例问题就定位了如果没找到只能说在深度k内没问题。利用对称性如果系统中有多个相同组件可以尝试利用对称性减少状态空间nuXmv支持对称性规约但配置较复杂。调整后端引擎go命令可以使用-a参数选择不同的算法如go -a BDD(默认) 或go -a IC3。对于某些模型IC3可能比BDD更高效。7.4 关于ASSIGN、INVAR、TRANS的优先级与语义这是nuXmv建模的核心难点务必理解ASSIGN init(x) : v;定义变量x的初始值。必须满足所有INVAR。ASSIGN next(x) : expr;定义变量x的下一个值。这是一个非确定性的定义。expr可以是一个集合用{v1, v2}表示case语句的不同分支也可以给出不同值。它定义了所有“可能的”下一个值。INVAR expr;定义了一个条件该条件必须在所有可达状态上为真。它限制了系统的状态空间。TRANS expr;定义了一个条件该条件必须在所有状态转移上为真。它限制了next关系。expr中可以使用next()函数。执行流程首先找到所有满足init()赋值和所有INVAR的状态作为初始状态集。对于每个当前状态s计算每个变量x的next(x)表达式得到一组可能的“下一个值”集合。用TRANS条件过滤这些可能的转移。只有那些使得TRANS表达式为真的(当前状态, 下一状态)对才是合法的转移。如果对于某个状态s不存在任何下一状态能满足TRANS则状态s是死锁状态。简单策略对于初学者建议主要使用ASSIGN来定义确定性的或非确定性的转移用INVAR来定义状态不变式。谨慎使用全局的TRANS因为它会与ASSIGN中的next定义交互容易引入死锁或非预期行为。可以把TRANS看作是对整个系统转移关系的额外全局约束。经过这个完整的交通灯控制器实例的建模、验证、调试和修正你应该对nuXmv的工作流程有了一个扎实的感性认识。记住模型检测是一个迭代过程建模 - 验证 - 分析反例 - 修正模型/性质 - 再验证。那个自动生成的反例轨迹是你最好的调试伙伴。从这个小系统开始你可以尝试建模更复杂的东西比如带有传感器和紧急模式的交通灯、简单的通信协议如交替位协议、或者资源锁管理器。每完成一个模型你对形式化描述和机器验证的理解就会加深一层。