2. 设备状态机建模基础
在半导体设备软件中，状态机不是一张“好看的流程图”，而是对设备行为的一种可执行约束。它规定了设备在任意时刻允许处于哪些状态、什么条件下可以离开当前状态、离开时执行什么动作、进入新状态后又必须满足哪些不变量。把这些要素形式化，才能让软件在晶圆传输、工艺执行、报警恢复等场景中保持确定性，避免出现“机械手已伸出但腔体仍在抽真空”这类危险并发。
形式化定义通常用五元组描述：M = (S, E, T, A, G)。其中 S 是状态集合，E 是事件集合，T ⊆ S × E × S 是迁移关系，A 是动作集合，G 是守卫条件集合。一个具体迁移可写成 t: (s_from, e, g, a, s_to)，含义是：当系统处于 s_from、事件 e 到达且守卫 g 为真时，执行动作 a 并进入 s_to。守卫条件是一个返回布尔值的谓词，只决定“能不能迁”，不产生副作用；动作则是迁移发生时真正改变物理量或软件变量的操作，例如打开阀门、置位标志、启动定时器。把“判断”和“执行”分离，是状态机可测试、可审计的关键。
事件分为外部事件与内部事件。外部事件来自操作员、上位机 MES 或安全回路，如 Start、Abort、InterlockOpen；内部事件来自定时器、传感器或软件自身，如 Timeout、PressureReached、WaferLoaded。半导体设备中，事件往往带有优先级：安全类事件（如 EmergencyStop）必须能在任意状态抢占，而工艺类事件只能在特定状态被接受。因此建模时通常把安全事件单独抽成一条“全局迁移”，不受普通守卫限制。
下面这张图给出本节核心要素之间的关系，以及五个典型状态的迁移骨架。图中实线表示正常工艺路径，虚线表示异常或维护路径，守卫条件标注在迁移旁。
五个典型状态的语义必须写清楚，否则不同工程师对“Ready”的理解会不一致。下面给出可直接落到代码注释或设计文档中的定义。
| 状态 | 语义 | 进入条件（守卫） | 典型动作 |
|---|---|---|---|
| Idle | 设备上电但未完成初始化，不接收晶圆 | 上电复位完成 | 加载参数、自检 |
| Ready | 初始化通过，允许接收晶圆与启动工艺 | 无报警、气压/真空正常、伺服使能 | 点亮就绪灯、开放传输口 |
| Processing | 正在执行工艺配方，禁止人工干预传输 | 有片、腔体洁净、配方已加载 | 开阀、控温、计时、采集 |
| Error | 检测到故障，输出被安全限制 | 任意状态收到 Fault 或安全事件 | 关阀、断加热、置报警码 |
| Maintenance | 离线维护，软件与执行机构隔离 | 故障清除且人工确认 | 禁用自动、开放手动 |
建模时最容易出错的是“动作放在哪里”。一个常见错误是把“打开传输阀”写在守卫里，导致每次求值都产生副作用。正确做法是：守卫只读传感器与标志位，动作只在迁移被确认后执行一次。另一个错误是忽略迁移的原子性——在半导体设备中，Processing → Error 的动作必须包含“关闭工艺气体”和“停止加热”，且这两步要么都做，要么都不做，否则会留下安全隐患。实现上可用一个事务式动作块，或让状态机引擎在进入 Error 时统一执行安全动作集。
bool canStart() { return hasWafer && vacuumOK && !alarmActive; }。这样单元测试可以直接构造输入验证真假，而不需要启动真实设备。
下面给出一个可参考的状态迁移表，用于把设计意图固化成可评审的成果。表中每一行对应一条迁移，字段与五元组一一对应，便于直接转成代码或测试用例。
迁移表（示例，参数为合理假设）
ID 源状态 事件 守卫条件 动作 目标状态
t1 Idle InitOK 无报警 ∧ 气压≥0.5MPa 使能伺服、加载配方 Ready
t2 Ready Start 有片 ∧ 腔体洁净 ∧ 配方有效 开传输阀、启动计时 Processing
t3 Processing ProcessEnd 计时到 ∧ 温度达标 关阀、降温、记录批次 Ready
t4 Processing Fault 压力超限 ∨ 温度超限 关阀、断加热、置报警码 Error
t5 Error Repair 故障清除 ∧ 人工确认 复位报警、禁用自动 Maintenance
t6 Maintenance MaintainDone 维护完成 ∧ 自检通过 重新使能、清维护标志 Ready
t7 任意 EmergencyStop 无（最高优先级） 断使能、关所有阀、急停 Error
有了这张表，就可以逐条检查：是否存在无法到达的状态、是否存在没有出口的状态、安全事件是否覆盖所有状态、守卫条件是否引用了未定义的变量。例如 t7 的源状态是“任意”，实现时通常用状态机引擎的全局迁移机制，而不是在五个状态里各写一遍。再比如 t3 与 t4 都从 Processing 出发，事件不同、守卫不同，引擎按事件匹配即可，不会冲突；但如果两个迁移事件相同而守卫可能同时为真，就必须定义优先级，否则行为不确定。
最后要强调状态不变量。每个状态除了“能做什么”，还要声明“必须始终成立什么”。Ready 的不变量是“无报警且伺服使能”；Processing 的不变量是“传输阀状态与配方阶段一致”；Error 的不变量是“所有工艺输出处于安全值”。把不变量写成断言，在每次迁移后检查，可以在开发阶段尽早暴露建模缺陷，而不是等到流片或量产时才由设备事故暴露。状态、迁移、事件、动作、守卫这五个要素加上不变量，才构成一个可用于半导体设备自动运行的完整状态机模型。