运行时验证是根据系统的运行轨迹来判定系统性质是否得到满足的一种轻量级验证技术，是保证系统运行时行为正确性的重要方法。因此，在航空航天、高铁、核电、医疗和工控等安全攸关领域的系统验证中有着广泛的应用^[1–2]。

由于现代安全攸关系统正变得日趋庞大和复杂，系统拥有大量的随机行为特征^[3]，因此，随机系统运行时验证受到了广泛研究和关注^[4–5]。Filieri等^[6]针对自适应软件系统运行环境的改变可能使系统不满足属性规约，提出一种运行时验证方法，该方法使用连续时间马尔可夫链建模系统可靠性，使用概率计算树逻辑规约系统属性，对系统的可靠性进行运行时验证。Forejt等^[7]使用马尔可夫决策过程来建模系统，提出了系统模型的增量构造方法和基于强连通组件的策略迭代技术来优化运行时验证的性能。Bak等^[8]提出了在不可靠的网络通信下，信息物理融合系统的安全属性不变式运行时验证方法。Mao等^[9]使用混成自动机建模自适应巡航控制系统，使用CHARON建模语言规约安全属性，验证了自适应巡航控制系统运行时安全性。采样是减少运行时监控费用有效方法，为了处理采样序列丢失而引起的预测精度低的问题，Stoller等^[10]将采样序列作为隐马尔科夫模型（hidden Markov model，HMM）的观测序列，通过HMM前向算法估计由于采样而丢失的观测序列，该方法的系统属性验证算法需要计算属性自动机和系统模型组合状态的联合概率分布，计算效率低，难以满足在线监控的需求。为了提高计算效率，Kalajdzic等^[11]采用粒子滤波方法估计属性自动机和系统模型组合状态的联合概率分布，并通过实验验证粒子滤波方法消耗的内存和运行速度优于文献[10]中的方法，但随着系统模型的增大，粒子在状态上分布就越稀疏，为了保证计算精度，需要更多的粒子覆盖系统状态。

综上所述，目前的随机系统运行时验证都假设系统状态是可以直接观测的，实际上大多数复杂系统在运行时其状态是不可观测的^[10–11]。针对此问题，采用HMM对机系统建模，使用确定性有限自动机（deterministic finite automaton，DFA）规约系统安全属性，通过HMM和DFA的乘积来构造安全属性验证器，从而将状态不可观测的随机系统运行时验证问题约简到属性验证器上的概率推断问题。同时，提出了验证器的宽度优先构造算法和增量迭代安全性验证算法。

1 运行时验证框架

采用在线监控的方式对随机系统安全性进行验证^[12]。

状态不可观测的随机系统运行时安全性验证描述为：给定系统状态转换模型TS，系统安全属性 ${\varphi _{{\rm{safe}}}}$ 以及系统运行时的观测序列 ${o_{\rm{1}}},o_{\rm{2}},\cdots,{o_t}$ ，计算在 $t$ 时刻系统满足安全属性的概率 $P{r_t}(TS \vDash {\varphi _{{\rm{saf}}{\rm e}}}|{o_{\rm{1}}},o_{\rm{2}},\cdots,{o_t}) $ 。图1给出运行时安全性验证框架。

图1中的虚线框是监控器单元，监控器由事件接收器和属性验证器组成。其中，事件接收器接收系统的观测序列进行预处理后输入到属性验证器进行验证，属性验证器输出当前系统安全属性被满足的概率。系统安全属性的否定使用DFA A表示，用以识别系统执行中违反安全属性的有限前缀。属性验证器是一个含有不安全状态的HMM，由系统模型HMM H和属性自动机A的乘积表示。 ${P_{{\rm{th}}}}$ 表示系统安全概率的阈值。

事件接收器将从系统获取的观测数据存放缓存中，再进行预处理，最后输入到安全性验证器。触发监控器工作的方式主要有事件触发和时间触发（采样）两种^[13]。对于事件触发方式，其预处理较简单，只需按时间戳先后进行排序后输入到属性验证器；对于时间触发方式，其预处理比较复杂，需要按时间戳先后排序、消除重复采样数据、填充丢失序列等操作。由于提出的验证框架主要关注属性验证器的构造和验证算法，触发监控器工作方式使用事件触发。

2 属性验证器

使用DFA^[14]和HMM^[15]构造属性验证器，下面给出两种模型的定义。

定义1 　一个DFA是如下形式的五元组 ${A} =$ $ (Q,\varSigma,\delta ,{q_0},F)$ 。其中：

1） $Q$ 为有限的，非空的状态集合；

2） $\varSigma$ 为输入字母表， $\varSigma$ =2^AP，AP为原子命题集合；

3） $\delta :Q \times \varSigma\to Q$ 为一个状态转换函数；

4） ${q_0} \in Q$ 为一个初始状态；

5） $F \subseteq Q$ 为接受状态的集合。

如果在 $A$ 中 $\forall q \in Q$ ， $\forall B \in {2^{{{AP}}}}$ 都有 $\left| {\delta \left( {q,B} \right)} \right| = 1$ ，那么 $A$ 是一个完全的DFA。一个完全的DFA对于每个输入字 $\sigma \in {\left( {{2^{{{AP}}}}} \right)^\omega }$ 都存在一个唯一的运行与之对应。

定义2 　一个HMM是一个元组 $H=(S,$ $ {{P}},{\iota _{{\rm{init}}}},L,O,\mu )$ 。其中：

1） $S$ 是有限的，非空的状态集合；

2） $P:S \times S \to \left[ {0,1} \right]$ 是状态转换概率分布函数，对于 $\forall s \in S,\displaystyle\sum\limits_{s' \in S} {P(s,s') = 1} $ ；

3） ${\iota _{{\rm{init}}}} :S \to \left[ {0,1} \right]$ 是初始状态概率分布函数， $\displaystyle\sum\limits_{s \in S} {{\iota _{{\rm{init}}}}(s)} = 1$ ；

4） $L:S \to {2^{{{AP}}}}$ 是标签函数；

5） $O$ 是系统可观测符号的有限集合，即系统模型输出的有限集合；

6） $\mu :S \times O \to \left[ {0,{\rm{ }}1} \right]$ 是状态的可观测符号概率分布函数，对于 $\forall s \in S,\displaystyle\sum\limits_{o \in O} {\mu (s,o) = 1} $ 。

$\mu \left( {s,o} \right)$ 或 ${\mu _s}\left( o \right)$ 表示系统在状态 $s$ 产生观测 $o$ 的概率，相同的观测可能由多个不同的系统状态产生，因此，在已知目前观测的情况下系统的状态是不确定的。

安全属性验证器定义为一个HMM和DFA的乘积自动机，系统安全属性是基于观测符号描述，即DFA的输入字母表 $\varSigma\subseteq O$ 。

定义3 　安全属性验证器定义为 $ H= (S,P,{\iota _{{\rm{init}}}},L,$ $O,\mu )$ 和 $A= (Q,\varSigma ,\delta ,{q_0},F)$ 的乘积自动机 ${M} = (S',P',$ $\iota {'_{{\rm{init}}}},F',O,\mu ')$ 。其中：

1） $S' = S \times Q$ ，属性验证器状态集合；

$2\;)P'( \left\langle {} s,q \right\rangle{} , \left\langle {} s',q' \right\rangle{} ) = \left\{ \begin{aligned}&P(s,s') \displaystyle\sum\limits_{t \in T} {{\mu _s}\left( t \right)} ,\;{\rm{if}}\;T \ne \varnothing{\text{；}} \\&0,\;\;{\rm{otherwise}}\end{aligned} \right.$ 表示状态转换概率分布，其中， $T = O(s') \cap {\delta ^{ - 1}}(q,q')$ ， $O(s')$ 表示在状态 $s'$ 观测字母的集合， ${\delta ^{ - 1}}(q,q') \subseteq \varSigma$ 表示在 ${A}$ 中从状态 $q$ 到 $q'$ 的输入字母的集合；

3） $F' = S \times F$ ，接受状态集合；

4） $\iota {'_{{\rm{init}}}}( \left\langle {} s,q \right\rangle{} ) = \left\{ \begin{array}{l}\!\!\!\!\!{\iota _{{\rm{init}}}}(s) \displaystyle\sum\limits_{t \in T} {{\mu _s}\left( t \right),\;{\rm{if}}\;T \ne \varnothing }, \\\!\!\!\!\!0,\;\;{\rm{otherwise}}\end{array} \right.$ 表示属性验证器初始状态概率分布，其中， $T = O(s) \cap $ ${\delta ^{ - 1}}({q_0},q)$ ；

5） $\mu '( \left\langle {} s,q \right\rangle{} ,o) = {\mu _s}(o),o \in T$ ，表示状态 $ \left\langle {} s,q \right\rangle{} $ 的观测符号概率分布。

根据定义可知，属性验证器M是一个含有接受状态集的HMM，算法1给出了M构造算法，首先构造验证器的所有初始状态，然后，从初始状态出发，采用宽度优先算法构造M，其中， ${S_{\!{\rm{init}}}}$ 表示待处理状态的集合， $S'$ 表示已处理状态的集合， $succ\left( q \right)$ 表示在 ${A}$ 中状态 $q$ 的后继集合。算法1运行结束后， $S'$ 中的状态就是M的状态，同时，M中不包含从初始状态不可达的状态以及与监控属性无关的状态，避免了联合概率分布的计算，约简了验证器的规模。验证器可以静态构造，不占用系统运行时的资源，系统只需要保存验证器模型，无需保存HMM和DFA模型。

算法1 　属性验证器构造算法

输入： ${H}$ 、 ${A}$ ；

输出： ${M}$ 。

1.　 ${S_{{\rm{init}}}} = S' = P' = \iota {'_{{\rm{init}}}} = F' = \mu ' = \varnothing $ ；

2.　for each $s \in S$ do

3.　　for each $q \in succ\left( {{q_0}} \right)$ do

4.　　　 $T = O(s) \cap {\delta ^{ - 1}}({q_0},q)$ ；

5.　　　if （ $T \ne \varnothing $ ）

6.　　　　 ${S_{{\rm{init}}}} = {S_{{\rm{init}}}} \cup \{ \left\langle {s,q} \right\rangle \} $ ；

7.　　　　 $\iota {'_{{\rm{init}}}}( \left\langle {} s,q \right\rangle{} ) = {\iota _{{\rm{init}}}}(s)\displaystyle\sum\limits_{t \in T} {{\mu _s}\left( t \right)} $ ；

8.　　　　 $\mu '( \left\langle {} s,q \right\rangle{} ,o) = {\mu _s}\!\left( o \right),o \in T$ ；

9.　　　end if

10.　　end for

11.　end for

12.　while ${S_{{\rm{init}}}} \ne \varnothing $ do

13.　get a state $\left\langle {s,q} \right\rangle \in {S_{{\rm{init}}}}$ and $ \left\langle {} s,q \right\rangle{} \notin F'$ ；

14.　for each $s' \in S$ and $P(s,s') > 0$ do

15.　　for each $q' \in succ\left( q \right)$ do

16.　　　 $T = O(s') \cap {\delta ^{ - 1}}(q,q')$ ；

17.　　　if （ $T \ne \varnothing $ ）

18.　　　 $P'( \left\langle {} s,q \right\rangle{} , \left\langle {} s',q' \right\rangle{} ) = P(s,s')\displaystyle\sum\limits_{t \in T} {{\mu _s}\left( t \right)} $ ；

19.　　　　 $\mu '( \left\langle {} s,q \right\rangle{} ,o) = {\mu _s}\left( o \right),o \in T$ ；

20.　　　　if $\left\langle {s',q'} \right\rangle \notin (S' \cup {S_{{\rm{init}}}})$

21.　　　　　 ${S_{{\rm{init}}}} = {S_{{\rm{init}}}} \cup \{ \left\langle {s',q'} \right\rangle \} $ ；

22.　　　　if （ $q' \in F'$ ）

23.　　　　　 $F' = F' \cup \{ \left\langle {} s',q' \right\rangle{} \} $ ；

24.　　　　　 $P'( \left\langle {} s',q' \right\rangle{} , \left\langle {} s',q' \right\rangle{} ) = 1$ ；

25.　　　　end if

26.　　　end if

27.　　end for

28.　end for

29.　 ${S_{{\rm{init}}}} = {S_{{\rm{init}}}}\backslash \{ \left\langle {s,q} \right\rangle \} $ ；

30.　 $S' = S' \cup \{ \left\langle {} s,q \right\rangle{} \} $ ；

31.　end while

通过分析语句18的最大执行次数确定算法1的最坏时间复杂度。如果所有状态都从初始状态可达，那么，算法需要处理的状态数是 $\left| S \right| \times \left| O \right|$ 。对于每个状态 $ \left\langle {} s,q \right\rangle{} $ ，最坏情况是：在 ${H}$ 中状态 $s$ 到每个状态 $s' \in S$ 都存在有向边，同样，在 ${A}$ 中状态 $q$ 到每个状态 $q' \in Q$ 都存在有向边，那么，状态 $ \left\langle {} s,q \right\rangle{} $ 的直接后继状态数是 $\left| S \right| \times \left| O \right|$ 。因此，语句18执行的次数 ${\left( {\left| S \right| \times \left| O \right|} \right)^2}$ 。语句18中，求和运算 $\displaystyle\sum\limits_{t \in T} {{\mu _s}\left( t \right)} $ 的最大执行次数是系统可观测值的有限集合 $O$ 的势。由此可知，算法1的最坏时间复杂度是 $O\left( {\left| O \right| \times {{\left( {\left| S \right| \times \left| O \right|} \right)}^2}} \right)$ 。

3 增量迭代安全性验证算法

先给出信念状态的定义，再给出增量信念状态更新算法来计算系统安全性概率。

定义4 　信念状态（belief state）是指在时刻 $t$ ，已知系统的观测序列 ${o_1},{o_2},\cdots,{o_t}$ ，属性验证器M处在状态 $s$ 的概率。形式化表示为：

${b_t}(s) =Pr (s|{o_1},{o_2},\cdots,{o_t}; M),\forall s \in S',\sum\limits_{s \in S'} {{b_t}(s)} = 1{\text{。}}$

由于观测值是从系统的不同状态发出的，因此，无法知道系统目前所处的准确状态，即M所处的状态。但是，根据系统的历史观测，通过HMM的前向算法能够计算系统的信念状态。HMM的前向算法是一种批处理算法^[15]，需要保存当前观测值之前的整个观测序列才能给出监控结论，随着系统观测序列的增长，前向算法消耗的内存和计算时间也将增长，难以满足实时验证需求。为此，提出一种在线增量迭代安全性验证算法，一旦收到一个新的观测值，立即更新信念状态并给出已观测到的整个有限序列的监控结论，无需保存当前观测值之前的整个观测序列。

增量信念状态更新以在线递推方式计算系统信念状态，在 $t$ =1时，系统信念状态 ${b_{\rm{1}}}(s)$ 取决于初始状态分布和初始观测值 ${o_1}$ ，根据HMM的齐次马尔科夫假设可知，系统在 $t$ 时刻的信念状态 ${b_t}(s)$ 只依赖于 ${b_{t{\rm{ - 1}}}}(s)$ 和当前的观测 ${o_t}$ 。图2给出了属性验证器的信念状态更新过程，引理给出了 ${b_t}(s)$ 和 ${b_{t{\rm{ - 1}}}}(s)$ 之间的关系。

引　理 　给定系统的历史观测序列 ${o_1},{o_2},\cdots,{o_t}$ ，M的信念状态更新函数 ${b_t}(s)$ 可表示为如下递推公式：

${b_t}(s) = \left\{ \begin{aligned}&\frac{{\iota {'_{{\rm{init}}}}(s)\mu {'_s}\left( {{o_1}} \right)}}{{{{\textit{z}}_1}}},t = 1;\quad\quad\quad\quad\quad\quad\quad\quad\\&\frac{{\displaystyle\sum\limits_{{s_{t - 1}} \in S'} {{b_{t - 1}}({s_{t - 1}})P'({s_{t - 1}},s)\mu {'_s}\left( {{o_t}} \right)} }}{{{{\textit{z}}_t}}},t >1{\text{)}}\end{aligned} \right.$

(1)

式中， ${{\textit{z}}_1} = \displaystyle\sum\limits_{s \in S'} {\iota {'_{{\rm{init}}}}(s)\mu {'_s}\left( {{o_1}} \right)} $ ， ${{\textit{z}}_t} = \displaystyle\sum\limits_{s \in S'} { \displaystyle\sum\limits_{{s_{t - 1}}} \in S'} {{b_{t - 1}}}({s_{t - 1}})\cdot$ $\;\;\;\;\;{P'({s_{t - 1}},} $ ${ { s)\mu {'_s}\left( {{o_t}} \right)} } $ 。

证明：根据信念状态的定义和贝叶斯定理^[16]可得 $t$ =1时信念状态：

$\begin{aligned}{b_{\rm{1}}}\!\!\left( s \right) = & Pr(s|{o_{\rm{1}}}) = \frac{{Pr(s,{o_{\rm{1}}})}}{{Pr({o_{\rm{1}}})}}=\\& \frac{{Pr(s)Pr({o_{\rm{1}}}|s)}}{{ \displaystyle\sum\limits_{s \in S'} {Pr(s,{o_{\rm{1}}})} }} = \frac{{\iota {'_{{\rm{init}}}}(s)\mu {'_s}\left( {{o_{\rm{1}}}} \right)}}{{ \displaystyle\sum\limits_{s \in S'} {\iota {'_{{\rm{init}}}}(s)\mu {'_s}\left( {{o_{\rm{1}}}} \right)} }}{\text{。}}\end{aligned}$

假设在 $t$ >1时，已知 ${b_{t - 1}}({s_{t - 1}})$ 和当前的观测 ${o_t}$ ，则系统在 $t$ 时刻的信念状态：

$\begin{aligned}[b]{b_t}\left( s \right) = & Pr(s|{o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_t}) = \frac{{Pr(s,{o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_t})}}{{Pr({o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_t})}}= \\&Pr(s,{o_t}|{o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_{t{\rm{ - 1}}}})\frac{{Pr({o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_{t{\rm{ - 1}}}})}}{{Pr({o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_t})}}\end{aligned}$

(2)

式中，

$\begin{aligned}[b]& Pr(s,{o_t}|{o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_{t{\rm{ - 1}}}}) = \sum\limits_{{s_{t - 1}} \in S'} {Pr(s,{s_{t - 1}},{o_t}|{o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_{t{\rm{ - 1}}}})}= \\&\quad \sum\limits_{{s_{t - 1}} \in S'} {Pr({s_{t - 1}}|{o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_{t{\rm{ - 1}}}})} Pr(s,{o_t}|{s_{t - 1}},{o_{\rm{1}}},{o_{\rm 2}},\cdots,{o_{t{\rm{ - 1}}}})=\\&\quad \sum\limits_{{s_{t - 1}} \in S'} {{b_{t - 1}}\left( {{s_{t - 1}}} \right)} Pr(s|{s_{t - 1}})Pr({o_t}|s)=\\&\quad \sum\limits_{{s_{t - 1}} \in S'} {{b_{t - {\rm{1}}}}\left( {{s_{t - 1}}} \right)P'({s_{t - 1}},s)\mu {'_s}\left( {{o_t}} \right)}\quad\quad\quad\quad\quad\quad\quad\quad\;\end{aligned}$

(3)

$\begin{aligned}[b]&\frac{{Pr({o_{\rm{1}}},{o_{\rm 2}},\cdots\!,{o_{t{\rm{ - 1}}}})}}{{Pr({o_{\rm{1}}},{o_{\rm 2}},\cdots\!,{o_t})}}\!\!=\!\!\frac{{Pr({o_{\rm{1}}},{o_{\rm 2}},\cdots\!,{o_{t{\rm{ - 1}}}})}}{{Pr({o_{\rm{1}}},{o_{\rm 2}},\cdots\!,{o_{t{\rm{ - 1}}}})Pr({o_t}{\rm{|}}{o_{\rm{1}}},{o_{\rm 2}},\cdots\!,{o_{t{\rm{ - 1}}}})}}\!\!=\\&\frac{{\rm{1}}}{{Pr({o_t}{\rm{|}}{o_{\rm{1}}},{o_{\rm 2}},\cdots\!,{o_{t{\rm{ - 1}}}})}}{\rm{ = }}\frac{{\rm{1}}}{{ \displaystyle\sum\limits_{s \in S'} { \displaystyle\sum\limits_{{s_{t - 1}} \in S'} {Pr(s,{s_{t - 1}},{o_t}|{o_{\rm{1}}},{o_{\rm 2}},\cdots\!,{o_{t{\rm{ - 1}}}})} } }}\!\!=\\&\quad \frac{{\rm{1}}}{{\displaystyle\sum\limits_{s \in S'} {\displaystyle\sum\limits_{{s_{t - 1}} \in S'} {{b_{t - {\rm{1}}}}\left( {{s_{t - 1}}} \right)P'({s_{t - 1}},s)\mu {'_s}\left( {{o_t}} \right)} } }} = \frac{1}{{{{\textit{z}}_t}}}\qquad \;\;\;\;\;\;\;\;\;\;\;\end{aligned} $

(4)

将式（3）和（4）代入式（2），即可得到式（1）。

由于M中的接受状态集 $F'$ 是系统的不安全状态，在M构造过程中删除了从初始状态不可达状态以及与监控属性无关的状态，而这些状态对于 ${\varphi _{{\rm{safe}}}}$ 而言是安全状态，因此，已知系统观测序列 ${o_1},$ ${o_2},\cdots,{o_t}$ ， $t$ 时刻系统安全性的概率 $ P{r_t}( M \vDash {\varphi _{{\rm{saf}}{\rm e}}}|{o_1},{o_2}\!,\cdots,$ ${o_t}) =$ $1 -\displaystyle\sum\limits_{s \in F'} {{b_t}(s)} $ 。根据引理，算法2为根据系统的当前观测 ${o_t}$ 计算系统安全性概率的算法。

算法2 　安全性验证算法

输入：M和当前的观测 ${o_{\rm t}}$ ；

输出： $P{r_t}( M \vDash {\varphi _{{\rm{saf}}{\rm e}}}|{o_{\rm{1}}},{o_{\rm{2}}},\cdots,{o_t})$ 。

1.　if （t ==1） then

2.　　for each $s \in S'$ do

3.　　　 ${b_1}'(s) = \iota {'_{{\rm{init}}}}(s)\mu {'_s}\left( {{o_{\rm{1}}}} \right)$ ；

4.　　　 ${{\textit{z}}_1} + = {b_1}'(s)$ ；

5.　　end for

6.　　for each $s \in S'$ do

7.　　　 ${b_1}(s) = {b_1}'(s)/{{\textit{z}}_1}$ ；

8.　　end for

9.　else

10.　　for each $s \in S'$ do

11.　　　for each $s{'_{t - 1}} \in S'$ do

12.　　　　 $b{'_t}(s) + = {b_{t - 1}}({s_{t - 1}})P'({s_{t - 1}},s)\mu {'_s}\left( {{o_t}} \right)$ ；

13.　　　end for

14.　　　　 ${{\textit{z}}_t} + = b{'_t}(s)$ ；

15.　　end for

16.　　for each $s \in S'$ do

17.　　　 ${b_t}(s) = b{'_t}(s)/{{\textit{z}}_t}$ ；

18.　end for

19.　end if

20.　return $1 - \displaystyle\sum\limits_{s \in F'} {{b_t}(s)} $ ；

从算法2中可以看出语句12的执行次数最多，可以通过分析语句12的最大执行次数确定算法的最坏时间复杂度。由语句10~15可知，语句12的执行次数为 ${\left| {S'} \right|^2}$ ， $\left| {S'} \right|$ 表示M的状态数，因此，算法2的时间复杂度为 $O\left( {{{\left| {S'} \right|}^2}} \right)$ 。使用HMM前向算法计算信念状态，其时间复杂度为 $O\left( {\left| T \right| \times {{\left( {\left| S \right| \times \left| O \right|} \right)}^2}} \right)$ ，其中， $T$ 表示观察序列的长度，在运行时验证中，系统的观测序列随时间增长，因此， $T$ 也随时间不断增长。由于在M构造过程中删除了从初始状态不可达状态以及与监控属性无关的状态，因此， $\left| {S'} \right| \le \left| S \right| \times \left| O \right|$ ，增量迭代算法明显由于HMM前向算法。

4 实验分析

通过随机多线程并发访问共享数据对象的案例^[11]验证作者提出的方法是否能够有效地计算系统安全性概率，探测安全属性的违背以及评估算法的时空性能。为了防止数据不一致性或数据污染，通过加锁机制实现线程并发访问共享数据。一个共享数据对象包含锁字段、保护字段和非保护字段。随机线程运行时可观察变量的集合是{LOCK，UNLOCK，PROT，UNPORT}，其中，LOCK表示线程获得了目标对象的锁，UNLOCK表示线程释放了目标对象的锁，PROT表示线程访问目标对象的受保护字段，UNPROT表示线程访问目标对象的非保护字段。

4.1 实验设置

随机线程的HMM模型如图3所示，该线程以较小的概率违背锁原理，每个状态的可观测变量及相应的概率如表1所示。

待验证的安全属性为“线程获得目标对象的锁后才能访问目标对象的受保护字段”，对应的探测安全属性违背的DFA如图4所示，其中，输入字母表Σ={LOCK，UNLOCK，PROT，UNPORT}， ${q_1}$ 为初始状态。根据线程的HMM模型和属性自动机DFA模型，利用算法1可构造的安全属性验证器如图5所示，图5中，双圆圈表示验证器的接受状态，即系统的不安全状态。实验运行在Intel core i5双核2.4 GHz CPU，8 G内存，64位Win10操作系统上。通过HMM MATLAB工具箱模拟系统运行，按照以下步骤产生长度为 $T$ 的观测序列并输入到监控器的。生成步骤如下：

1）按照初始状态分布 ${\iota _{{\rm{init}}}}$ 产生状态 ${s_1}$ ；

2）令 $t$ =1；

3）根据状态 ${s_t}$ 的观测分布 $\mu \left( {{s_t},.} \right)$ 生成 ${o_t}$ ；

4）根据状态 $ \left\langle {} {s_t},{q_t} \right\rangle{} $ 的转移概率分布 ${P}\left( {{s_t},\;}\right. $ $\left. {{s_{t + 1}}} \right)$ 生成 ${s_{t + 1}}$ ；

5）令 $t = t + 1$ ，如果 $t < T$ ，转步骤3），否则终止。

4.2 安全属性验证

系统安全性概率阈值为0.90，模拟系统运行产生1 000个观测序列，当系统进入不安全状态时进行复位操作，重新从初始状态运行。图6给出了系统安全性概率随着观测序列的变化，从图6中可以看出，由于提出的安全性验证算法采用增量迭代计算，所以能实时反映系统安全性概率的变化情况，并且在运行中探测到3次系统安全属性违背。

表2列出了当系统违背安全属性时，获取系统最近的长度为10的观测序列和当前系统安全性概率。从第1行和第3行观测序列可以看出，系统释放目标对象锁之后访问了保护字段，从第2行观测序列可以看出，系统没有获得了目标对象的锁就访问了保护字段，显然这3种情况都违背了安全属性并且本文方法都能够快速准确地探测到。

4.3 方法性能比较

将本文的方法和HMM前向算法^[11]和粒子滤波算法^[12]在时间和空间性能进行了比较。通过不断增大系统模型的状态数，并且构造不同状态数的无向完全图作为系统模型，图3中的状态转换和状态的可观测符号是等概率分布，待验证属性由图3中的DFA表示。为了保证粒子滤波算法验证结果和本文方法具有相同的精度，不同的状态数对应的粒子数分别为：400、800、1 200、1 600、2 000。表3给出了3种算法的执行时间和内存消耗情况。

从表3可知，粒子滤波算法执行时间优于HMM前向算法，但消耗的内存较大，本文方法的执行时间和内存消耗明显优于其他两种算法。当系统状态达到80时，HMM前向算法和粒子滤波算法的执行时间和内存消耗显著增加；当系统状态达到100时，本文方法的执行时间只有粒子滤波算法的14.5%，消耗内存空间仅为HMM前向算法的22.7%。获得上述实验结果的主要原因是：1）通过属性验证器的构造约简了HMM和DFA组合状态数，而粒子滤波算法和前向算法是直接基于系统模型和属性自动机的组合状态进行联合概率分布的计算；2）安全性验证算法是在线增量计算的，每次仅处理一个观测，而粒子滤波算法和前向算法需要处理和保存当前观测之前的序列。

5 结　论

由于随机系统的复杂性，在设计阶段的模型检测和测试技术难以确保其正确性，运行时仍会发生违反安全属性的行为。针对随机系统在运行时状态是不可直接观测的，提出了运行时安全性验证方法。首先，构造了运行时验证框架，通过HMM对系统建模，使用DFA规约系统安全属性的否定，两者的乘积自动机作为运行时属性验证器并且给出验证器的构造算法。然后，提出了一种增量迭代的安全性验证算法。实验结果表明提出的方法能正确、快速地探测系统违背安全属性的行为。本文方法没有考虑混成系统特征，下一步的工作将使用HMM混合模型建模随机混成系统并对该类系统进行验证。