2. Stateflow建模语义精要

Stateflow 的静态分析质量，首先取决于建模语义是否被准确表达。Polyspace 并不会“猜测”设计意图，它读取的是 Stateflow 编译后形成的语义结构：哪些状态是互斥的、哪些是并行的、转移由什么事件触发、守卫条件在什么时刻求值、动作在转移的哪个阶段执行。如果这些语义在模型里含糊，静态分析结果就会出现大量误报或漏报。因此，理解 Stateflow 的语义元素及其到代码生成、静态分析的映射关系，是质量工程的第一道关口。

状态：互斥与并行的两种基本语义

状态（State）是 Stateflow 的基本执行单元。一个状态可以包含 entry、during、exit 三类动作，分别在该状态被激活、保持激活、被退出时执行。状态之间最关键的语义区分是互斥（OR）与并行（AND）：互斥父状态下同一时刻只有一个子状态处于激活；并行父状态下所有子状态同时激活。这一区别直接决定代码生成结果——互斥结构生成 if-else 或 switch 分支，并行结构生成多个可同时执行的代码块，并影响 Polyspace 对共享变量访问的并发判断。

状态还可以携带状态动作与状态输出。例如 entry: mode = 1; 会在进入状态时赋值，而 during: count = count + 1; 会在每个执行步中累加。静态分析会检查这些动作是否在所有路径上初始化了变量，以及是否存在未定义读取。

转移、事件、条件与动作的时序语义

转移（Transition）连接源状态与目标状态，其完整语义由四部分组成：事件（Event）、条件（Condition）、条件动作（Condition Action）、转移动作（Transition Action）。典型写法为：

[cond] {cond_action} / trans_action

其中事件触发转移的求值时机，条件决定是否真正发生转移，条件动作在条件成立后、转移生效前执行，转移动作在转移生效后执行。这个顺序在代码生成中体现为：先判断事件与条件，再执行条件动作，最后执行转移动作并更新激活状态。Polyspace 会沿着这条时序链检查条件动作与转移动作之间是否存在变量状态不一致，例如条件动作修改了某变量，而转移动作又基于旧值做判断。

事件分为输入事件、本地事件和广播事件。输入事件来自外部输入端口，本地事件在 Stateflow 内部触发，广播事件可跨层次传播。静态分析需要确认事件是否被正确声明、是否在期望的执行步中被触发，以及是否存在事件丢失导致的死状态。

层次结构与并行机制

Stateflow 支持多层嵌套：父状态可以包含子状态图，子状态图内部又可继续嵌套。层次结构带来两个关键语义：默认转移决定进入父状态时首先激活哪个子状态；历史节点（History Junction）决定重新进入父状态时是否恢复上次激活的子状态。这两者在代码生成中分别映射为初始化分支和状态记忆变量，Polyspace 会检查历史节点是否在所有路径上都有明确定义的恢复目标。

并行机制则通过并行父状态实现。并行子状态之间没有转移关系，它们同时运行，共享数据时必须考虑执行顺序。Stateflow 默认按图形从左到右、从上到下的顺序执行并行状态，但这一顺序在代码生成中可能被优化，静态分析会据此判断是否存在数据竞争或未同步访问。

语义到静态分析的映射要点

把上述语义放到 Polyspace 分析流程中，可以归纳出几条关键映射规则。第一，状态动作的完整性：每个状态的 entry 动作是否覆盖了所有输出变量的初始化，Polyspace 会沿激活路径检查未初始化读取。第二，转移条件的可达性：如果某条转移的条件在数学上恒假，或依赖的事件从未被触发，该转移就是不可达的，Polyspace 会报告死代码。第三，并行状态的数据竞争：当两个并行子状态同时读写同一变量且没有明确的执行顺序保证时，Polyspace 会标记潜在竞争。第四，历史节点的恢复一致性：历史节点必须指向明确的子状态，否则重新进入父状态时行为未定义。

一个可操作的语义检查清单

下面这份清单可以直接用于模型评审或静态分析前的自检，字段和判断依据均围绕 Stateflow 语义与 Polyspace 检查项设计：

需要强调的是，Stateflow 的语义并不是孤立存在的，它最终会映射为 C 代码中的分支、赋值和函数调用。Polyspace 的分析对象正是这些生成后的代码，但它对语义的理解来自 Stateflow 的编译中间表示。因此，建模阶段把语义写清楚，等价于在源头控制了静态分析的信噪比。对于层次结构与并行机制，尤其要注意默认转移、历史节点和并行执行顺序这三处，它们最容易在代码生成中被“隐式处理”，也最容易在静态分析中产生难以定位的告警。