形式化定义软件动态更新

柔光的暖阳◎ 2024-04-01 15:01 44阅读 0赞

## 形式化定义软件动态更新 ##

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

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

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

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

#### 1.2  ( P i , E i , R i ) (P\_i,E\_i,R\_i) (Pi,Ei,Ri) 定义 ####

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

#### 1.3 `DEADLOCK_FREE` 需求 ####

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

#### 1.4 需求规约限制 ####

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

1.  全局不出现（global absence） □ ¬ ∅ \\square \\neg \\empty □¬∅ 以及 全局都出现（global universality） □ ∅ \\square \\empty □∅
2.  全局响应性（global response）  □ ( ∅ → ⋄ ψ ) \\square (\\empty \\rightarrow \\diamond \\psi) □(∅→⋄ψ)

### 2. 正确的系统版本 ###

#### 2.1 当  ⊨ \\vDash ⊨ 右边是集合 ####

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

#### 2.2 正确的系统版本 定义 ####

一个版本为  i i i 的系统  ( P i , E i , R i ) (P\_i,E\_i,R\_i) (Pi,Ei,Ri) 是正确的当且仅当我们有  P i ∣ ∣ E i ⊨ R i P\_i||E\_i \\vDash R\_i Pi∣∣Ei⊨Ri

### 3. 软件动态更新方案 ###

#### 3.1 软件动态更新方案 定义 ####

一个软件动态更新方案是一个集合  D S = \{ ( s , t ) ∣ s ∈ S P 1 ∧ t ∈ S P 2 \} DS=\\\{(s,t)|s\\in S\_\{P\_1\} \\wedge t \\in S\_\{P\_2\}\\\} DS=\{(s,t)∣s∈SP1∧t∈SP2\}。 ( s , t ) ∈ D S (s,t)\\in DS (s,t)∈DS 表示通过一个特殊的  d s u dsu dsu 动作，从旧的程序状态  s s s 跳转到新的程序状态  t t t。

#### 3.2 软件动态更新方案 理解 ####

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

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

### 4. 软件动态更新 `LTS` 模型 ###

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

给定一个软件动态更新的方案  D S DS DS ，一个软件动态更新的 `LTS`  D = ( S D , A D , Δ D , s 0 , D ) D=(S\_D,A\_D,\\Delta\_D,s\_\{0,D\}) D=(SD,AD,ΔD,s0,D) 是将改动态更新方案应用到新旧程序模型  P 1 P\_1 P1 和  P 2 P\_2 P2 中得到的 `LTS` 。其中， S D = S P 1 ∪ S P 2 ∪ \{ ( s , d s u , t ) ∣ ( s , t ) ∈ D S \} S\_D=S\_\{P\_1\}\\cup S\_\{P\_2\} \\cup \\\{(s,dsu,t)|(s,t)\\in DS\\\} SD=SP1∪SP2∪\{(s,dsu,t)∣(s,t)∈DS\}， s 0 , D = s 0 , P 1 s\_\{0,D\}=s\_\{0,P\_1\} s0,D=s0,P1 。

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

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

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

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

一个软件动态更新 `LTS`  D D D 是正确定，当且仅当，我们有  D ∣ ∣ E 2 D||E\_2 D∣∣E2 不会造成死锁并且  D ∣ ∣ E 2 D||E\_2 D∣∣E2 不会造成死锁并且  D ∣ ∣ E 2 ⊨ □ ( A F T E R \_ D S U → R 2 ) D||E\_2 \\vDash \\square(AFTER\\\_DSU \\rightarrow R\_2) D∣∣E2⊨□(AFTER\_DSU→R2) 成立。一个软件动态更新方案是正确的，当且仅当它能产生一个正确的软件动态更新 `LTS` 模型。

### 6. 包含软件动态更新的  t r a c e trace trace ###

#### 6.1 包含软件动态更新的  t r a c e trace trace 定义 ####

给定两个版本的系统  ( P 1 , E 1 , R 1 ) (P\_1,E\_1,R\_1) (P1,E1,R1) 和  ( P 2 , E 2 , R 2 ) (P\_2,E\_2,R\_2) (P2,E2,R2) 以及一个动态更新方案，一个包含软件动态更新的 `trace` 是  D ∣ ∣ E 2 D||E\_2 D∣∣E2 中的一个  t r a c e   π = l 0 , l 1 , . . . , l i , . . . trace \\thinspace \\pi=l\_0,l\_1,...,l\_i,... traceπ=l0,l1,...,li,...，其中有且仅有一个  i i i 使得  l i l\_i li 是  d s u dsu dsu 动作。

#### 6.2 包含软件动态更新的  t r a c e trace trace 解释 ####

直觉上来看，在 `dsu` 动作之前，系统执行的 `trace` 是在  P 1 ∣ ∣ E 1 P\_1||E\_1 P1∣∣E1 上执行的，在 `dsu` 动作之后，是在  P 2 ∣ ∣ E 2 P\_2||E\_2 P2∣∣E2 执行的。换句话说，对于这种的包含软件动态更新的  t r a c e   π trace \\thinspace \\pi traceπ 来说，它的长度为  i i i 的前缀是  P 1 ∣ ∣ E 1 P\_1||E\_1 P1∣∣E1 中的一个合法 `trace` 的前缀，并且  l i + 1 , . . . l\_\{i+1\},... li\+1,... 是  P 2 ∣ ∣ E 2 P\_2||E\_2 P2∣∣E2 中的合法的 `trace` 的一个后缀。一个包含软件动态更新的  t r a c e   π trace \\thinspace \\pi traceπ 是正确的，当且仅当有， π ⊨ □ ( A F T E R \_ D S U → R 2 ) \\pi \\vDash \\square (AFTER\\\_DSU \\rightarrow R\_2) π⊨□(AFTER\_DSU→R2) 。

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