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

### 嵌入式系统设计中的行为近似 #### 1. 引言 在嵌入式系统设计中，为了更好地描述和分析系统行为，需要使用不同的跟踪代数来表示不同抽象层次的行为。本文将介绍三种跟踪代数，包括它们的定义、操作以及它们之间的关系，还会涉及到同态、保守近似和逆近似等概念。 #### 2. 跟踪代数的定义 ##### 2.1 度量时间跟踪代数 度量时间跟踪代数中，部分跟踪和完整跟踪的连接有明确的定义。若 $x_3 = x_1 · x_2$，则 $x_1$ 是 $x_3$ 的前缀。当定义 $x_3 = (\gamma_1, \delta_3, f_3)$ 时，有 $\delta_3 = \delta_1 + \delta_2$，并且对于所有 $a \in A$： - 当 $0 \leq \delta \leq \delta_1$ 时，$f_3(a)(\delta) = f_1(a)(\delta)$； - 当 $\delta_1 \leq \delta \leq \delta_3$ 时，$f_3(a)(\delta) = f_2(a)(\delta - \delta_1)$。 ##### 2.2 非度量时间跟踪代数 在非度量时间跟踪代数的定义中，我们关注系统中事件发生的顺序，而非它们的绝对距离或位置。这对于描述嵌入式系统编程语言的语义很有用，因为它可以从特定的实时实现中抽象出来。 - **标记偏序（Labeled partial order, lpo）**：一个标记偏序 $L = (V, \Sigma, \leq, \mu)$ 由以下部分组成： 1. 顶点集 $V$，通常用于建模事件； 2. 字母表 $\Sigma$，通常用于建模动作，如整数 3 到达端口 Q、IC - 7 的引脚 13 转变为 4.5 伏等； 3. $V$ 上的偏序 $\leq$，通常 $e \leq f$ 表示事件 $e$ 在时间上必然先于事件 $f$； 4. 标记函数 $\mu : V \to \Sigma$，为顶点分配符号，每个标记事件代表其标记动作的一次发生，同一动作可能有多次发生。 - **偏序多重集（Pomset）**：是 lpo 的同构类，记为 $[V, \Sigma, \leq, \mu]$。 - **全序偏序多重集（Tomsets）**：我们将自己限制在偏序为全序的 pomsets 上，称为 tomsets。 跟踪的形式为 $x = (\gamma, L)$，其中 $\gamma = (V_R, V_Z, M_I, M_O)$，$L$ 是 tomset。投影和重命名操作可以很容易地从动作扩展到 lpo 和跟踪。连接操作 $x_3 = x_1 · x_2$ 定义为当且仅当 $x_1$ 是部分跟踪，$\gamma_1 = \gamma_2$ 且 $\mu_1(max(V_1)) = \mu_2(min(V_2))$。 以下是连接操作的流程图： ```mermaid graph TD; A[x1 是部分跟踪] --> B{γ1 = γ2}; B -- 是 --> C{μ1(max(V1)) = μ2(min(V2))}; C -- 是 --> D[定义连接操作 x3 = x1 · x2]; B -- 否 --> E[不定义连接操作]; C -- 否 --> E; ``` ##### 2.3 前后时间跟踪代数 前后时间跟踪代数用于建模编程语言的非交互构造。在这个抽象层次上，我们只关心给定初始状态下代理的可能最终状态。 - 签名形式为 $\gamma = (V_R, V_Z)$，字母表 $A = V_R \cup V_Z$。 - 非退化状态 $s$ 是一个定义域为 $A$ 的函数，对于所有 $v \in V_R$，$s(v)$ 是实数；对于所有 $v \in V_Z$，$s(v)$ 是整数。还有一个退化的未定义状态 $\perp^*$。 - 部分跟踪