1. 课程导入与工程场景锚定

在嵌入式控制软件中，Stateflow 并不是一个“画流程图”的装饰工具，它承担的是离散控制逻辑的显式建模与可执行化。以电机控制为例，一个典型的控制器往往同时包含连续域算法（如电流环 PI、SVPWM 计算）和离散域逻辑（如启动、运行、降速、故障、复位）。前者适合用 Simulink 框图表达，后者若用普通框图实现，会迅速退化为大量 Switch、Relational Operator 和 Memory 模块的“连线迷宫”，可读性、可验证性和可追溯性都很差。Stateflow 的价值在于：用状态、转移、条件、动作和层次结构，把“什么时候做什么”变成一张可执行、可分析、可生成代码的状态机。

本课程围绕一个贯穿全课的典型模型展开：三相无刷直流电机控制状态机。它的顶层状态包括 Init、Idle、Align、Run、Decel、Fault 和 Recover。输入信号包括 startCmd、stopCmd、speedRef、speedFdbk、overCurrent、overTemp、hallValid；输出包括 pwmEnable、dutyCmd、faultCode、stateOut。这个模型规模适中，既包含正常控制流，也包含故障与恢复路径，非常适合用来演示 Polyspace 静态分析如何发现“仿真不一定触发、但代码里真实存在”的缺陷。

Polyspace 静态分析的价值定位，需要从“测试的盲区”来理解。动态仿真和台架测试只能覆盖实际执行到的路径。假设 Run 状态下有一个转移条件 speedFdbk > speedRef + 200，如果测试中反馈从未超过参考值 200 rpm，这条转移就从未被激活，其中的数组越界、除零、溢出或未初始化读取就不会暴露。Polyspace 基于抽象解释和形式化方法，在不运行代码的前提下，对变量取值范围、指针指向、数组索引、控制流可达性进行全局推理，能够回答三类关键问题：运行时错误是否存在（如除零、越界、溢出）、代码是否不可达或死逻辑、变量是否可能未初始化或越界。对 Stateflow 生成的代码而言，这三类问题恰好对应状态机中最隐蔽的风险。

质量工程目标可以拆成四个可检查的维度。第一，功能安全：故障状态必须可达且优先级正确，不能出现“过流了却进不了 Fault”的死转移。第二，确定性：同一输入序列必须产生同一状态序列，不能依赖未初始化变量或执行顺序的偶然性。第三，可追溯性：每条转移条件、每个动作都能追溯到需求条目，Polyspace 的检查结果可作为评审证据。第四，可维护性：状态层次清晰，默认转移、历史节点、并行状态的使用有明确规范，避免后续修改引入回归缺陷。

把这张图放在工程语境里看，Stateflow 的每个状态对应一个明确的控制阶段，每条转移对应一个可判定的条件，每个动作对应一次输出更新。Polyspace 要做的，就是沿着这些转移和动作，检查所有可能的取值组合下是否会出现运行时错误。例如 dutyCmd = speedRef / speedFdbk 这类计算，如果 speedFdbk 在 Align 阶段可能为 0，Polyspace 会直接报出除零风险，而仿真若恰好没跑到该分支，问题就会被带到实车上。

本课程后续将按“建模规范 → 静态分析配置 → 结果判读 → 缺陷修复 → 回归验证”的路径推进，但每一节都围绕这个电机状态机展开，不脱离真实对象谈工具。读者在学完后，应能独立完成三件事：第一，用 Stateflow 正确表达带故障与恢复的控制逻辑；第二，用 Polyspace 对生成代码做系统性静态检查；第三，根据检查结果定位并修复缺陷，形成可复用的质量证据链。