嵌入式系统设计中的行为近似

### 嵌入式系统设计中的行为近似 #### 1. 逆函数与多态性 在嵌入式系统设计中，函数 $\Psi_{inv}$ 并不一定需要对所有的 $p'$ 都进行定义。例如，若模型 $Q'$ 包含了一些无法在模型 $Q$ 中精确表达的信息，就会出现这种情况。此时，$\Psi_{inv}$ 是一个部分函数，仅对在两个模型中都有精确表示的代理进行定义。当一个代理在 $Q$ 和 $Q'$ 中都有精确表示时，我们称它可以在这两个模型中无差别地使用，或者说它是多态的。这是因为该代理不会基于仅能在某一个计算模型中表达的信息对其行为进行假设。不过，一般来说，该代理在 $Q$ 和 $Q'$ 中的表示是不同的。这种概念扩展了我们在采用不同表示的模型之间复用代理的能力。 在一些例子中，从度量时间代理到非度量时间代理的近似的逆函数总是有定义的，它会将一个非度量时间代理转换为一个对应的度量时间代理，该度量时间代理会为其任何行为非确定性地选择一个给定的时间。这种非确定性是我们方法的典型特征，它有助于揭示在基于细化的设计方法中可用的自由度。同样，从前后置代理到非度量时间代理的保守近似的逆函数会构建一个具体化，其中每对初始和最终状态是通过沿时间轴重新排序动作来非确定性计算的。 保守近似会以（可能是部分的）细化映射的形式诱导出其自身的逆函数。这个逆函数是唯一确定的，并且由于保守近似的定义属性，$\Psi_{inv}$ 是一对一的。当限制在 $\Psi_{inv}$ 的像上时，函数 $\Psi_{l}$ 和 $\Psi_{u}$ 相等，并且是 $\Psi_{inv}$ 的逆函数。此外，当 $\Psi_{inv}$ 有定义时，它总是单调的。如果 $\Psi_{l}$ 或 $\Psi_{u}$ 也是单调的，那么它会在两个方向上保留代理的顺序。因此，逆函数会将抽象的计算模型（或者至少是其有定义的部分）嵌入到更具体的模型中，并且这种嵌入方式与所选择的抽象是一致的。同一模型之间的不同保守近似可能会诱导出不同的嵌入。这再次表明了为手头的问题选择正确抽象的重要性。实际上，嵌入的性质决定了一个模型如何根据另一个模型进行解释，并量化了在抽象过程中丢失的信息量。 #### 2. 嵌入式软件中的建模构造 ##### 2.1 使用前后置轨迹 嵌入式软件的一个基本特征是它与物理世界进行交互。顺序编程语言的传统公理或指称语义仅对终止程序的初始和最终状态进行建模。因此，这些语义不足以完全对嵌入式软件进行建模。然而，嵌入式应用中的许多代码主要进行计算或内部通信，而不是与物理世界进行交互。只要该模型能够与用于建模交互所需的更详细语义集成，那么就可以使用传统语义对这类代码进行适当的建模。前后置代理与传统语义非常相似。如前文所述，我们还可以将前后置代理嵌入到更详细的模型中。因此，我们可以在较高的抽象级别上对嵌入式应用的非交互部分进行建模，这种方式更简单、更自然，同时还能够集成精确的交互模型、实时约束和连续动态。 以开发用于控制发动机在切断区域的软件问题为例。汽车发动机的行为被划分为不同的运行区域，每个区域都有相应的控制动作以实现期望的结果。当驾驶员松开油门踏板时，发动机进入切断区域，此时要求发动机不产生扭矩。为了最小化由于突然降低扭矩而导致的动力传动系统振荡，闭环控制会使用精心定时的燃油喷射来抑制振荡。因此，这个控制问题是混合的，由离散（燃油喷射）和连续（动力传动系统行为）两个紧密相连的系统组成。 以下是一个嵌入式控制算法的示例代码： ```c 01. void control algorithm( void ) { 02. // state definition 03. struct state { double x1; double x2; double omega c; } current state; 04. // Init the past three injections (assume injection before cutoff) 05. double u1, u2, u3 = 1.0; 06. 07. loop forever { 08. await( action request ); 09. read current state( current state ); 10. compute sigmas( sigma m, sigma 0, current state, u1, u2, u3 ); 11. // update past injections 12. u1 = u2; u2 = u3; 14. // compute next injection signal 15. if ( sigma m < sigma 0 ) { 16. action injection( ); 17. u3 = 1.0; 18. } else { 19. action no injection( ); 20. u3 = 0.0; 21. } 22. } 23. } ``` 该代码展示了控制算法的顶层例程。虽然使用了类似 C 的语法，但语义进行了简化。控制器由一个喷射决策请求激活（每个完整的发动机循环都会发生一次）。该算法首先读取系统的当前状态（由动力传动系统上的传感器提供），预测喷射或不喷射对系统未来行为的影响，最后控制是否进行喷射。预测使用过去三次决策的值来估计未来状态的位置。控制算法涉及求解一个微分方程，这在调用 `compute sigmas` 时完成。在不喷射中间量燃油的情况下（即要么不喷射燃油，要么喷射最大量），可以实现接近最优的解决方案。因此，系统的唯一控制输入是 `action injection`（最大喷射）和 `action no injection`（零喷射）这两个动作。 编程语言中每个语句的语义由一个代理给出。为了简化语义，我们假设进程间通信是通过共享动作而不是共享变量来完成的。前后置代理具有形式为 $(\mathcal{V}_R, \mathcal{V}_Z)$ 的签名 $\gamma$。对于编程语言语句的语义，$\gamma$ 表示该语句出现的作用域中可访问的变量。对于声明局部变量的块，块中语句的代理在其签名中包含这些局部变量。块的代理是通过从语句的代理中投影掉局部变量而形成的。 两个语句的顺序组合被定义为相应代理的连接：连接的定义确保两个语句在中间状态上达成一致。对变量 $v$ 进行赋值的代理中的轨迹形式为 $(\gamma, s_i, s_f)$，其中 $s_i$ 是任意初始状态，$s_f$ 与 $s_i$ 相同，除了 $v$ 的值等于在状态 $s_i$ 中计算的赋值语句右侧的值（我们假设计算没有副作用）。 过程定义的语义由一个字母表为 $\{v_1, \ldots, v_r\}$ 的代理给出，其中 $v_k$ 是过程的第 $k$ 个参数（这些信号名称不一定与形式变量的名称相对应）。我们省略了如何从过程定义的文本构造这个代理的细节。对于我们的控制算法示例，过程调用 `proc(a, b)` 的语义是对 `proc` 定义的代理进行 $v_1 \to a$ 和 $v_2 \to b$ 重命名的结果。得到的参数传递语义是值 - 结果（即没有别名或引用），并且限制任何参数不能同时用于值和结果。也可以对更现实（且更复杂）的参数传递语义进行建模。 为了定义 `if-then-else` 和 `while` 循环的语义，我们定义了一个函数 `init(x, c)`，当且仅当谓词 $c$ 在轨迹 $x$ 的初始状态中为真时，该函数为真。其正式定义取决于所使用的特定轨迹代数。特别是，对于前后置轨迹，如果 $x$ 的初始状态为 $\bot^*$，则对于所有 $c$，`init(x, c)` 都为假。 对于 `if-then-else` 的语义，设 $c$ 为条件表达式，$P_T$ 和 $P_E$ 分别为 `then` 子句和 `else` 子句的可能轨迹集合。`if-then-else` 的可能轨迹集合为： $P = \{x \in P_T : \text{init}(x, c)\} \cup \{x \in P_E : \neg \text{init}(x, c)\}$ 需要注意的是，这个定义可以用于任何已经定义了 `init(x, c)` 的轨迹代数，并且它忽略了条件表达式 $c$ 计算不是原子操作的任何影响。 在 `w