1. 状态机等价与精化基础在嵌入式系统设计中状态机是最常用的建模工具之一。理解状态机之间的等价关系对于系统验证和逐步精化至关重要。我们首先需要区分两种基本的等价关系语言等价和仿真等价。语言等价关注的是外部可见行为。两个状态机M1和M2是语言等价的当且仅当它们对于所有可能的输入序列都能产生相同的输出序列集合。这种等价关系可以用形式化语言表示为L(M1) L(M2)其中L(M)表示状态机M的语言——所有可能的输入输出行为集合。然而语言等价在非确定性系统中存在局限性。如图14.3所示的例子中两个状态机虽然语言等价都能产生输出序列01或00但它们的内部决策机制不同导致在某些环境下不能互相替代。这就引出了更强的等价关系——仿真等价。提示在设计嵌入式系统时语言等价适合用于验证黑盒行为而仿真等价则更适合白盒验证确保实现细节与规范一致。2. 仿真关系详解2.1 仿真关系的形式化定义仿真关系是一种结构化的等价验证方法。给定两个状态机M1和M2我们说M1模拟M2记作M2 ≤ M1如果存在一个关系S ⊆ S2 × S1S2和S1分别是M2和M1的状态集合满足初始状态对应(initialState2, initialState1) ∈ S状态转移保持对于所有(s2,s1) ∈ S和所有输入xM2的每个可能转移(s2,x)→(s2,y2)都能被M1的某个转移(s1,x)→(s1,y1)匹配使得(s2,s1) ∈ Sy2 y1这个定义确保了M1可以跟踪M2的所有可能行为包括非确定性选择。2.2 仿真关系的构建方法构建仿真关系通常采用协同归纳(co-induction)的方法初始时将初始状态对加入关系S对于S中的每个状态对(s2,s1)检查所有可能的输入x a. 对M2从s2出发的每个可能转移找到M1从s1出发的对应转移 b. 确保输出相同且新状态对也满足仿真关系重复步骤2直到关系S不再扩大表14.1展示了图14.3中M1模拟M2的完整仿真关系M2状态M1状态eafbhbgcid2.3 仿真关系的性质仿真关系具有几个重要性质自反性任何状态机都模拟自身传递性如果M1模拟M2且M2模拟M3则M1模拟M3非对称性M1模拟M2并不意味着M2模拟M1非唯一性两个状态机之间可能存在多个不同的仿真关系3. 语言等价与仿真关系的比较3.1 语言包含与仿真定理14.1指出如果M1模拟M2则L(M2) ⊆ L(M1)。这意味着仿真关系比语言包含更强——它不仅要求所有行为都被包含还要求这些行为可以通过结构化的方式产生。考虑图14.2中的三个状态机(a)和(b)是语言等价的(c)的语言包含(a)和(b)的语言(b)模拟(a)(c)模拟(b)因此通过传递性(c)也模拟(a)3.2 何时需要仿真关系在以下场景中仅验证语言等价是不够的需要建立仿真关系非确定性系统验证确保实现的所有非确定性选择都符合规范逐步精化验证每个设计步骤都保持了系统属性组件替换确保新组件在任意环境下都能保持系统行为安全性验证特别是涉及无限行为或liveness属性时4. 双模拟(Bisimulation)4.1 双模拟的定义双模拟是比仿真更强的等价关系。两个状态机M1和M2是双模拟的如果存在一个关系S ⊆ S1 × S2使得S和它的逆S⁻¹都是仿真关系即M1模拟M2且M2模拟M1双模拟保证了两个状态机不仅在行为上等价在内部结构上也完全对称。4.2 双模拟的性质双模拟具有以下特点对称性如果M1与M2双模拟则M2也与M1双模拟是等价关系满足自反性、对称性和传递性保持所有CTL*属性包括线性和分支时序逻辑公式5. 在嵌入式系统设计中的应用5.1 设计流程中的验证在实际嵌入式系统设计中这些等价关系可以用于规范验证确保高级规范与需求一致实现验证检查代码或硬件实现是否符合规范优化验证确认优化后的设计保持原始语义组合验证验证组件集成后保持全局属性5.2 典型应用场景交通灯控制器如图3.10和图3.12所示验证确定性实现与非确定性规范的等价性中断处理验证ISR实现满足时序和功能要求协议实现确保通信协议实现符合抽象规范调度器设计验证实时调度策略满足时序约束6. 注意事项与常见问题6.1 仿真验证中的陷阱非完全抽象仿真关系只保证被模拟机器的属性在模拟机器中保持反之不一定成立状态空间爆炸对于复杂系统显式构建仿真关系可能不可行无限状态系统需要特殊技术处理如谓词抽象环境假设仿真关系依赖于环境行为的合理假设6.2 实用技巧分层验证先验证模块级仿真关系再组合成系统级关系抽象函数使用数学函数而非显式状态对来表示仿真关系工具辅助利用模型检查器如NuSMV、UPPAAL自动验证仿真关系反例引导当验证失败时分析反例改进设计或规范在实际工作中我经常发现工程师们容易混淆语言等价和仿真等价。一个典型的错误是假设语言等价的系统可以随意互相替换这在非确定性系统中尤其危险。正确的做法是对于确定性系统语言等价通常足够但对于非确定性系统必须建立仿真关系才能确保安全替换。