形式化定义软件动态更新

形式化定义软件动态更新

使用 LTS 来对程序以及它对应的环境进行建模，使用 FLTL 来描述需求规约。

1. 系统，程序，环境以及需求

1.1 系统，程序，环境以及需求 的定义

一个系统有一个程序和一个环境构成。程序的行为由 LTS $P$ 定义。环境的行为由 LTS $E$ 定义。系统的需求通过 FLTL 公式的一个集合 $R$ 定义。

1.2 $(P_i,E_i,R_i)$ 定义

我们使用下标来表示程序，环境以及需求的版本号。因为在一个系统中，这三个部分总是一同出现的。所对于版本为 $i$ 的系统，我们使用一个三元组 $(P_i,E_i,R_i)$ 来表示。

1.3 DEADLOCK_FREE 需求

由于我们显然是不希望程序和环境的交互进入死锁状态，为了简明起见，所以我们默认需求中包含了无死锁 DEADLOCK_FREE 这以特性，而不明确的表示出来。

1.4 需求规约限制

将需求规约限制分为了两类：

1. 全局不出现（global absence）$\square \neg \varnothing$ 以及 全局都出现（global universality）$\square \varnothing$
2. 全局响应性（global response） $\square (\varnothing \to \diamond \psi )$

2. 正确的系统版本

2.1 当 $\models$ 右边是集合

一个版本的系统的正确性是说这个版本的系统能够满足它的需求。当给定一个需求集合 $R$ 以及一个 LTS $S$ ，为了简洁起见，我们用 $S\models R$ 来表示 $S\models {\wedge }_{\varnothing \in R}\varnothing$。也就是说，当 $\models$ 右侧的 $R$ 为集合的时候，我们认为是 ${\wedge }_{\varnothing \in R}\varnothing$ 的缩写。

2.2 正确的系统版本 定义

一个版本为 $i$ 的系统 $(P_i,E_i,R_i)$ 是正确的当且仅当我们有 $P_i||E_i\models R_i$

3. 软件动态更新方案

3.1 软件动态更新方案 定义

一个软件动态更新方案是一个集合 $DS=\{(s,t)|s\in S_{P_1}\wedge t\in S_{P_2}\}$。$(s,t)\in DS$ 表示通过一个特殊的 $dsu$ 动作，从旧的程序状态 $s$ 跳转到新的程序状态 $t$。

3.2 软件动态更新方案 理解

这里说的状态是 LTS 的抽象状态，其实在最终的验证软件动态更新的正确性的时候，还是使用的 $trace$ 。用这些抽象状态是为了方便表述。

我们使用 $dsu$ 来表示特殊的软件动态更新的动作。如果程序或者环境模型中的动作包含了关键字 $dsu$ 的话，我们可以通过重命名的方式将这些动作更换成其他名字。

4. 软件动态更新 LTS 模型

4.1 软件动态更新 LTS 模型 定义

给定一个软件动态更新的方案 $DS$ ，一个软件动态更新的 LTS $D=(S_D,A_D,{\Delta }_D,s_{0,D})$ 是将改动态更新方案应用到新旧程序模型 $P_1$ 和 $P_2$ 中得到的 LTS 。其中，$S_D=S_{P_1}\cup S_{P_2}\cup \{(s,dsu,t)|(s,t)\in DS\}$，$s_{0,D}=s_{0,P_1}$ 。

4.2 软件动态更新的方案 与 软件动态更新 LTS

软件动态更新的方案和软件动态更新 LTS 有着对应关系，软件动态更新 LTS 有更加直觉的显示效果，所以在后面示例中我们将只给出软件动态更新 LTS 模型，并不显示区分这两个概念。

5. 正确的软件动态更新 LTS 和方案

5.1 正确的软件动态更新 LTS 和方案 定义

一个软件动态更新 LTS $D$ 是正确定，当且仅当，我们有 $D||E_2$ 不会造成死锁并且 $D||E_2$ 不会造成死锁并且 $D||E_2\models \square (AFTER\_DSU\to R_2)$ 成立。一个软件动态更新方案是正确的，当且仅当它能产生一个正确的软件动态更新 LTS 模型。

6. 包含软件动态更新的 $trace$

6.1 包含软件动态更新的 $trace$ 定义

给定两个版本的系统 $(P_1,E_1,R_1)$ 和 $(P_2,E_2,R_2)$ 以及一个动态更新方案，一个包含软件动态更新的 trace 是 $D||E_2$ 中的一个 $trace\pi =l_0,l_1,...,l_i,...$，其中有且仅有一个 $i$ 使得 $l_i$ 是 $dsu$ 动作。

6.2 包含软件动态更新的 $trace$ 解释

直觉上来看，在 dsu 动作之前，系统执行的 trace 是在 $P_1||E_1$ 上执行的，在 dsu 动作之后，是在 $P_2||E_2$ 执行的。换句话说，对于这种的包含软件动态更新的 $trace\pi$ 来说，它的长度为 $i$ 的前缀是 $P_1||E_1$ 中的一个合法 trace 的前缀，并且 $l_{i+1},...$ 是 $P_2||E_2$ 中的合法的 trace 的一个后缀。一个包含软件动态更新的 $trace\pi$ 是正确的，当且仅当有，$\pi \models \square (AFTER\_DSU\to R_2)$ 。

当我们有一个正确的软件动态更新的方案之后，我们可以产生一个正确的软件动态更新的 LTS 。根据定义，我们可以知道在这个软件动态更新的 LTS 中可能的所有 trace 都是正确的。那么当程序和环境在交互执行的时候，系统的执行一定是在某一个可能的 trace 上。那么这时候程序就可以被正确的动态更新了。正如我们前文说过，这样的正确的软件动态更新方案是通过静态分析得到的，是一个悲观保守的方案，因为在静态的模型检验中它只包含正确的动态更新的 trace 。