2. 控制逻辑与验证对象建模
虚拟验证的第一步不是打开仿真软件，而是把“设备到底怎么动作”这件事从图纸、程序、工艺描述里抽出来，变成计算机能执行、能判断对错的模型。工业设备的控制逻辑通常以四种形态存在：继电器回路、PLC梯形图、状态机、时序逻辑。它们描述的是同一件事的不同侧面，建模时要先识别当前需求属于哪一种表达，再决定用什么模型去承载。
四种逻辑表达的本质区别
继电器逻辑是物理触点的串并联，核心是“通/断”和“自锁/互锁”。它的可验证模型通常用布尔方程或触点网络表示，例如启动按钮 SB1 与停止按钮 SB2 控制接触器 KM1：
KM1 = (SB1 + KM1) · SB2 · FR
// SB1 常开启动，KM1 自锁，SB2 常闭停止，FR 热继电器常闭保护PLC梯形图把继电器逻辑软件化，但增加了扫描周期、定时器、计数器、边沿检测等元素。梯形图的“能流”从左母线流向右母线，同一时刻的触点状态取决于上一扫描周期的输出，这一点在建模时必须显式表达，否则仿真结果会与真实PLC不一致。
状态机适合描述设备的工作模式切换，例如“待机→手动→自动→报警→停机”。它的关键参数是状态集合、迁移条件、迁移动作和初始状态。时序逻辑则关注信号在时间轴上的先后关系，例如“夹紧到位后延时0.5s才允许主轴启动”，这类约束用状态机表达会显得笨重，用时间轴或时序约束表达更直接。
从需求到模型的关键抽象步骤
以一台“气动压装设备”为例，工艺要求是：操作员双手按下启动按钮后，气缸下行压装，压力达到设定值并保压2s，然后气缸返回，取出工件。这个描述里包含三类信息：安全约束（双手按钮）、动作顺序（下行→保压→返回）、参数约束（压力设定值、保压时间）。
第一步是定义输入输出变量。输入包括：左启动按钮 SB_L、右启动按钮 SB_R、上限位 SQ_UP、下限位 SQ_DN、压力开关 PS、急停 ES。输出包括：电磁阀 YV_DOWN、YV_UP、指示灯 HL_RUN。每个变量都要明确是常开还是常闭、是瞬时信号还是保持信号。
第二步是选择主模型。这个设备的动作顺序明确、状态数量有限，适合用状态机做主模型，再用时序约束补充保压时间。状态集合可以定义为：IDLE（待机）、DOWN（下行）、PRESS（压装保压）、UP（返回）、FAULT（故障）。迁移条件如下表所示。
| 当前状态 | 迁移条件 | 迁移动作 | 目标状态 |
|---|---|---|---|
| IDLE | SB_L=1 且 SB_R=1 且 SQ_UP=1 | YV_DOWN=1 | DOWN |
| DOWN | SQ_DN=1 | 启动保压定时器 T1=2s | PRESS |
| PRESS | PS=1 且 T1 完成 | YV_DOWN=0, YV_UP=1 | UP |
| UP | SQ_UP=1 | YV_UP=0, HL_RUN=0 | IDLE |
| 任意 | ES=1 或 PS 超限 | 所有输出复位 | FAULT |
第三步是补充时序约束。状态机只能表达“先做什么后做什么”，但“保压必须持续2s”这种时间量需要单独建模。可以在 PRESS 状态中挂一个定时器，迁移条件写成“PS=1 且 T1≥2s”。如果工艺要求“压力达到后0.3s内必须开始保压计时”，则要增加一个最大响应时间约束，用断言表达为：PS上升沿 → T1启动 ≤ 0.3s。
模型可验证性的三个判据
一个模型能不能用来做虚拟验证，要看它是否满足三个条件。第一是可执行：给定一组输入序列，模型能确定性地产生输出序列，不能有“可能动作也可能不动作”的歧义。第二是可观测：每个关键状态和输出都能被记录或查询，否则无法判断对错。第三是可判定：验证目标能写成明确的通过/失败条件，例如“在 ES=1 后 100ms 内所有输出必须为0”。
常见建模陷阱
第一个陷阱是把梯形图的扫描周期当成瞬时响应。真实PLC中，输入采样、程序执行、输出刷新是分阶段进行的，如果模型假设“输入变化立即影响输出”，在高速信号或短脉冲场景下会得到错误结论。建模时至少要保留一个扫描周期的延迟，或者明确标注“本模型忽略扫描周期影响”。
第二个陷阱是状态机缺少“异常迁移”。很多初学者只画正常流程，忘记急停、超时、传感器失效等分支。验证时一旦注入故障，模型就卡在某个状态无法退出。正确做法是给每个状态都检查全局异常条件，或者在状态机外层加一个故障监控层。
第三个陷阱是时序约束只写“延时”，不写“超时”。例如“等待到位信号”如果没有超时上限，模型在传感器故障时会永远等待。工程上通常给每个等待动作配一个监控定时器，超时后进入 FAULT 状态并报警。