电梯门不会夹人，靠测试够吗？聊聊形式化验证的硬骨头

9月23号下午，南京软件大道一栋写字楼的小会议室里，空调开得挺足，我却听得后背发凉。对面团队在评审一套工业门控固件，测试报告摊在桌上，覆盖率98%。有人问：都这样了，还上形式化验证干嘛？

我当场就想翻白眼。不是对测试有意见。测试很重要，天天跑，救命。可测试能逮住虫子，却没法宣布虫子绝迹。你跑了一万条用例，第一万零一条路径照样可能藏着关门指令和开门指令同时生效的鬼故事。电梯门不会夹人？靠测试够吗？说实话，不够。

覆盖率98%，为什么我还是心里发毛

覆盖率98%，为什么我还是心里发毛

那套门控逻辑不复杂，听起来像小儿科：红外遮挡、开门按钮、关门按钮、检修模式、电机正反转。可组合一多，人脑就糊了。检修模式下按关门，红外又恰好抖动，按钮还有机械回弹——这几个条件叠在一起，固件会不会短暂给关门电机上电？测试同事拍胸脯说没见过。没见过不等于不存在，对吧。

这里就撞上形式化验证的入口了。别把它想成高冷论文词。形式化验证，说白了就是用数学方法证明或证伪一个系统模型是否满足你写下的规约。规约是你对“不能出事”的精确描述，不是口头需求，不是“注意安全”。模型呢，是把代码或电路抽象成状态和迁移。然后让工具去搜：有没有一条路径，能走到你不想看到的状态。

它和测试的差别，像抽考和把题库全做一遍。测试选样本，形式化验证在模型里做穷举或推理。对。就是数学。冷冰冰的，但有时候真管用。

把“不会夹人”写成一条数学句子

评审会上我拿白板画了个小状态机。门控有开、关、停、故障几个状态，按钮和传感器是输入，电机输出是动作。接着写属性：只要红外遮挡有效，关门电机就不能得电；开门和关门请求同时出现时，系统不能同时响应两个方向；故障状态必须能回到安全停止态。写属性这一步，最考验人。属性写歪了，后面全白搭。

工具跑起来后，吐出一条反例路径。具体得让人冒汗：检修模式切进来，红外信号在去抖窗口里抖了一下，关门按钮的回弹被当成第二次按下，状态机从“检修停”跳到“关门预备”，再跳到“关门输出”。测试用例里没人把这三个条件串起来。你说气不气？

工业电梯门控状态机模型检测反例路径图

这就是模型检测的日常。工具不是神仙，它干的事很朴素：把状态迁移图摊开，按属性去搜反例。搜到了，给你一条具体路径；搜不到，在模型和抽象都靠谱的前提下，才敢说属性成立。定理证明则是另一条路，靠人给引理、推证明，适合状态空间大到没法穷举的场景。两条路都不轻松。

工具吐出一条反例，比吵架管用

我最喜欢形式化验证的地方，不是那张“证明通过”的截图，而是反例。反例是工程师之间的共同语言。你说“这里可能有问题”，对方说“不可能，我测过”。工具把路径一摆，输入序列一列，大家安静了。接下来要么改代码，要么改模型，要么承认环境假设写漏了。吵架成本直线下降。

落地时别一上来就啃整坨系统。切一块肉：一个互锁模块、一个总线仲裁器、一个寄存器配置序列。先做抽象，把无关的定时器和日志砍掉，保留影响安全属性的状态。然后写属性，跑模型检测。反例回来，人工判断是模型抽象错了，还是代码真漏了。修完再跑，进回归。轻量形式化可以塞进持续集成，别指望它天天跑全量，跑关键属性就挺香。

芯片RTL形式化验证属性规约与状态迁移图

别把它当银弹，它管不到的地方得认

误区一堆。有人以为形式化验证是“点个按钮，自动证明代码没bug”。哎，哪有这种好事。它证明的是模型满足规约，模型抽象漏了、规约写窄了、环境假设错了，证明通过也白搭。还有人把它当测试的替代品。真别。测试能覆盖物理噪声、时序抖动、驱动兼容性，这些形式化工具未必吃得下。两者是搭班子，不是抢饭碗。

状态爆炸也很现实。状态变量一多，搜索空间膨胀得让人怀疑人生。抽象做得好，能压下来；抽象做不好，工具跑三天三夜还在转。成本呢？工具链、建模能力、规约经验，都要人。团队没人懂时序逻辑，硬上就是给自己找罪受。

它的边界挺清楚：控制逻辑复杂、状态组合多、失效代价高的地方，值得上。芯片RTL、总线协议、操作系统内核、智能合约、轨道交通信号联锁，这些场景里形式化验证不是摆设。可需求本身模糊、界面交互为主、物理连续动态占大头，硬套形式化验证就有点拧巴。混合系统能碰，但门槛高，别装轻松。

地铁信号联锁系统形式化验证场景图

会散的时候，门外天已经擦黑。我下楼买了碗鸭血粉丝，脑子里还在转那条反例路径。形式化验证不神，也不便宜。它只是在你拍胸脯说“应该不会”的时候，冷冷递过来一张路径图：哥们，这条路上，门可能会夹人。