线性时序逻辑公式的可监控性量化算法

2020-12-11陈云云

小型微型计算机系统 2020年11期

陈云云，陈哲

(南京航空航天大学计算机科学与技术学院，南京 211106) (软件新技术与产业化协同创新中心，南京 211106) (高安全系统的软件开发与验证技术工业和信息化部重点实验室，南京 211106)

1 引言

运行时验证技术是一种轻量级的软件验证技术，它通过验证系统产生的有限行为序列是否满足某种约束来间接地验证系统的正确性[1,2].由于运行时验证技术不但可以有效地监测系统运行中的异常行为，而且可以在发现异常时发出警告或作出反应，因此，越来越多的学者对运行时验证进行了深入地探讨和研究[19-22].

软件验证领域常用线性时序逻辑(Linear Temporal Logic,LTL)这一形式化语言来描述系统需要满足的约束[23].然而，并不是所有的LTL公式都适合用于运行时验证.经过多年的研究，学者们常用可监控性和弱可监控性来衡量一个LTL公式在运行时验证领域的可用性.

可监控性最初是由Pnueli和Zaks提出的[3]，后来，Bauer对可监控性提出了一个更完善的定义并论述了在不同ω语言下可监控性判定问题的复杂度[5].2011年，Bauer和Leucker等人又基于LTL3[5]提出了监控器的概念，并概念性地给出了LTL公式对应监控器的构造方法[6].2014年，Diekert从拓扑学的角度阐述了可监控性问题，并证明了可监控性的判定问题是PSPACE完全问题[7].2018年，国内学者Chen Z.和Wu Y.指出在实际的运行时验证过程中，可监控性的要求过于严格，提出了弱可监控性[8]的概念，并结合Bauer等人提出的基于监控器的可监控性判定思想，提出了基于监控器的弱可监控性判定算法.

目前，关于可监控性和弱可监控性的判定算法主要有三种：基于监控器的判定算法[6]、基于公式重写的判定算法[9]和基于无限义务[9]的判定算法.其中，前两种算法是完备的算法，而第三种尚且不是一个完备的判定算法，但其可以和其他两种算法复合使用，起到加速的作用.

然而，在实际的运行时验证过程中，可监控性的要求过于严格，其要求对于任意的有限序列都能通过有限步的扩展使验证给出满足或违反的输出，这就导致一部分有价值的公式得不到应用.弱可监控性的提出避免了这一问题，但我们应该考虑到弱可监控性解决的仅仅是一个存在问题.因为其仅要求存在一条有限序列能通过有限步的扩展使验证给出满足或违反的输出即可.因此，我们无法得知一个弱可监控的公式中究竟存在多少条这样的有限序列.

综上，本文提出了概率可监控性的概念，然后重点研究了概率可监控性的求解算法，并在这些研究的基础上借助开源工具和C++语言进行了代码实现，并通过实验证明了算法的正确性.

2 理论知识

2.1 可监控性、弱可监控性

监控器M的输入是一条有限序列u∈Σ*，输出是B3集合中的一个值.对于给定的LTL公式φ，一定可以构造一个与其等价的监控器Mφ=(Q,Σ,δ,q0,λ)，使得对于∀u∈Σ*，都有[uφ]=λ(δ(q0,u))成立.

定义 2.可监控性[8](Monitorability).给定一个LTL公式φ，我们称φ是可监控的，当且仅当，对于∀u∈Σ*，都∃v∈Σ*，使得uvΣω⊆L(φ)或uvΣω∩L(φ)=∅成立.

定义 3.弱可监控性[8](Weak-Monitorability).给定一个LTL公式φ，我们称φ是弱可监控的，当且仅当，∃u,v∈Σ*，使得uvΣω⊆L(φ)或uvΣω∩L(φ)=∅成立.

从好前缀和坏前缀的角度来讲，如果对于任意的有限序列，其都能通过有限扩展成为公式φ的好前缀或坏前缀，那么φ是可监控的.例如，Xp∧Fq是可监控的，因为对于那些第二个符号为p的有限序列，只要其在未来延伸的某时刻满足了q，那么延伸后的序列就一定是Xp∧Fq的好前缀；而对于那些第二个符号为!p的有限序列，其已经是Xp∧Fq的坏前缀.如果存在一条有限序列能够通过有限扩展成为公式φ的好前缀或坏前缀，那么φ是弱可监控的.例如，Xp∧GFp是不可监控但弱可监控的，其等价的监控器如图1所示.

图1 公式Xp∧GFp的等价监控器Fig.1 Monitor of formula Xp∧GFp

对于那些第二个符号是p的有限序列，其已到达状态2，无论未来对其如何扩展都不可能使其成为公式的(好)坏前缀；但是，对于那些第二个符号是!p的有限序列，其就是公式的一个坏前缀，监控器可以快速地给出一个违反的判定.

2.2 马尔可夫链

定义 4.马尔可夫链[10](Markov Chain).马尔可夫链可以用一个五元组M=(Q,P,ιinit,AP,L)来表示，其中，Q是一个可数且非空的状态集合；P:Q×Q→[0,1]是迁移概率函数，且对于所有的q∈Q，有∑q′∈QP(q,q′)=1；ιinit:Q→[0,1]是初始分布，且有∑q∈Qιinit(q)=1；AP是原子命题的集合；L:Q→2AP是标签函数.

定义 5.σ-代数[10].σ-代数可以用一个集合对(Outc,E)来表示，其中，Outc是一个可数且非空的集合；∅∈E，E⊆2Outc，且E在补运算和可数个并(交)运算下是闭包的.

一般将Outc中的元素称作结果(outcome)，E中的元素称作事件(event).

定义 6.概率测度[10].概率测度是定义在σ-代数上的一个函数Pr:E→[0,1]，我们用Pr(E)表示事件E的概率测度，或简称事件E的概率.

定义 7.概率空间[10].概率空间可以用一个三元组(Outc,E,Pr)来表示，其中，(Outc,E)是一个σ-代数，Pr是定义在σ-代数上的概率测度.

PrM(Cyl(q0q1…qn))=ιinit(q0)·P(q0q1…qn)

(1)

其中，

(2)

特殊地，若有限路径的长度为0，则令P(q0)=1.

3 概率可监控性

为了确保对系统进行运行时验证时所使用的约束公式是合理的，需要对约束公式的可监控性和弱可监控性进行判定.但是，可监控性的要求过于严格，而弱可监控性又仅仅解决了“存在”的问题.

图2 监控器的结构图Fig.2 Structure diagram of monitor

弱可监控性仅仅解决了“存在”的问题.这里的“存在”问题指的是存在一条有限序列可以扩展为公式的好前缀或坏前缀，无论其存在一条、多条还是所有条.即只要不可监控的公式存在可监控的部分即可，不论其可监控部分的大小.

然而，通过研究，我们发现不同的弱可监控公式，其可扩展为公式的好前缀或坏前缀的有限序列的比例是不一样的，且可扩展为公式的好前缀或坏前缀的有限序列所占比例越大，其在运行时验证中就越有可能给出确定的判定结果，其利用价值也越大.但目前我们却无法计算出这些有限序列的比例.因此，为了量化公式的可监控性，我们提出了概率可监控性.

注意，上述定义中的有限序列就是有限符号序列，后文若无特殊说明，均遵循这个原则.

定义 9.概率可监控性. 给定公式φ及其等价监控器Mφ=(Q,Σ,δ,q0,λ)，我们称Mφ中可监控的有限序列条数占所有有限序列条数的比例为公式φ的可监控性概率，记为:

(3)

当公式是可监控的时，其可监控性概率是1；当公式是弱不可监控的时，其可监控性概率是0；当公式是不可监控但弱可监控的时，其可监控性概率的取值范围是(0,1).

4 概率可监控性的求解算法

4.1 直接求解的不可行性

当我们根据定义对可监控性概率进行计算时，个别公式的PrM(φ)可以直接地计算出来.例如，对于公式Xp∧GFp，其AP={p}，|AP|=2，其等价监控器(如图1)中长度为1的有限(符号)序列有=(2|AP|)1=2条，分别为∅和{p}，其对应监控器中的标签序列{true}，都是可监控的；长度为2的有限序列共有|Σ|2=4条，分别为∅∅、{p}∅、∅{p}和{p}{p}，其中，前两条对应监控器中的标签序列{true}{!p}，是可监控的，后两条对应监控器中的标签序列{true}{p}，是不可监控的；后面依此类推.经过我们上述的分析，我们发现当有限序列的长度大于等于2时，其有限序列被明显地分为两部分，一部分是那些第二个符号是{p}的有限序列，另一部分是那些第二个符号是∅的有限序列，因此，PrM(Xp∧GFp)可表示为：

但是，对于大多数的LTL公式，其可监控性概率是无法直接计算出来的.例如，对于计算机领域中常用的一个约束公式φ2=G((r1∧(u1U r2))→F(n2 U n1))∧((r→(t U u))U(t∨Gt))，其等价监控器M2如图3所示.

图3 公式φ2的等价监控器M2Fig.3 Monitor of formula φ2

图3中的每个状态都带有自身到自身的迁移，且图中还存在不同状态间互为后继的情况(状态0和1).在这样的情况下，随着有限序列长度n的增大，可监控的有限序列的情况就越复杂.例如，当n为1时，标签((!r& !t)|(!t&u))和(r& !t& !u)对应的有限序列是可监控的；当n为2时，标签((!r& !t)|(!t&u))2、(r& !t& !u)(t& !u)、(r& !t& !u)(!t& !u)、(r& !t& !u)(!t&u)和((!r& !t)|(!t&u))(r& !t& !u)对应的有限序列是可监控的.当有限序列的长度趋于无穷大时，可监控的有限序列就有无穷多种情况，无法计算.

4.2 概率可监控性问题的补问题

定义 10.ugly状态.给定一个监控器M=(Q,Σ,δ,q0,λ)，如果q∈Q满足λ(q)=?且对于∀r∈Post*(q)，都有λ(r)=?，则称状态q为ugly状态.

对于所有的公式，其不可监控的有限序列占有限序列的比例PrNM(φ)都可以表示为：

(4)

我们观察到，公式(3)和公式(4)中的分子分母有一定的特点，即其分母都是一个以|Σ|为公比的等比数列的和，随着长度n的增大，分母也不断增大，且当长度n趋于正无穷大时，分母也趋于正无穷大.这一特点与数学领域中的施托尔兹定理(The O′Stolz theorem)[11]非常契合.施托尔兹定理常用于处理数列不定式的极限问题，根据施托尔兹定理可得：

(5)

(6)

即公式φ的PrM(φ)(或PrNM(φ))就等于长度n趋于无穷大时的有限序列中，(不)可监控的有限序列的占比.

证明：首先，我们介绍数学领域中的施托尔兹定理[11]，该定理的具体描述如下：给定数列{an}、{bn}，若其满足：

下面，我们使用这一定理对公式(5)、公式(6)进行证明.首先，我们证明公式(5)的正确性.

所以，数列{An}、{Bn}满足条件③.

至此，公式(5)证明完毕.另外，关于公式(6)的证明方法与公式(5)的证明思想类似，此处不再赘述.

4.3 基于马尔可夫链的求解算法

通过分析，我们注意到不可监控的有限序列条数和监控器中每个边上标签对应的符号占比相关.例如，对于公式Xp∧GFp，长度为1的有限序列共2条，标签∅对应的符号集合占比0，不可监控的有限序列共2×0=0条；长度为2的有限序列共4条，标签{true}{p}对应的符号集合占比1×1/2=1/2，不可监控的有限序列2条；以此类推，长度为n的有限序列共2n条，标签{true}{p}{true}n-2对应的符号集合占比1×1/2×1n-2=1/2，不可监控的有限序列条数为2n×1/2=2n-1条.

此外，我们还注意到监控器本身就是一个特殊的确定性有限自动机，且其是完全的(complete)，即对于监控器中的任意状态，以该状态为源点出发的所有边上的标签对应的公式的析取等价于true(对应符号集合的并为Σ)，且任意两条边上标签对应的公式的合取等价于false(对应符号集合的交集为空集).而监控器和马尔科夫链的不同主要在于：一、马尔可夫链的迁移是通过概率分布选择的，而监控器的迁移是通过符号选择的；二、马尔可夫链的初始状态是根据其初始分布来确定的，而监控器中只有唯一的初始状态.下面，我们将解决上述两个问题，并给出将一个监控器描述为一个马尔可夫链的办法.

定义 11.给定一个监控器M=(Q,Σ,δ,q0,λ)，我们可以将其描述为一个马尔可夫链Mr=(Qr,Pr,ιinitr,APr,Lr)，其中，Qr=Q；Pr:Qr×Qr→[0,1]，对于所有的q∈Qr，有∑q′∈QrPr(q,q′)=1；ιinitr:Qr→[0,1]，ιinitr(q0)=1，对于任意的q∈Qr∧q≠q0，ιinitr(q0)=0，满足∑q∈Qrιinitr(q)=1；APr=AP；Lr:Qr→(2AP,λ)，λ:Q→B3.

在上述的定义中，我们解决了前面提的两个问题.第一个问题，由于监控器中的每个状态与其直接后继之间的迁移上的标签对应的符号的并集是符号全集2AP，且任意两条迁移对应的符号集合没有交集.因此，我们用每条迁移上标签对应的符号集合占符号全集Σ=2AP的比例来表示迁移概率.第二个问题，由于监控器是一个确定性的有限自动机，所以，其只有一个初始状态q0.因此，我们令ιinitr(q0)=1，且令其它的q∈Qr∧q≠q0，ιinitr(q)=0，这满足∑q∈Qrιinitr(q)=1.除此之外，我们将监控器中的状态输出添加到马尔科夫链的标签函数Lr中去(在图中，我们将状态输出和状态放在一起)，这是因为在后续算法的设计中，状态输出信息必不可少.通过上述定义，我们可以将监控器描述为一个标准马尔可夫链.

例如，图3的监控器M2可以描述为图4所示的马尔可夫链.

图4 监控器M2对应的马尔可夫链Fig.4 Markov chain of monitor M2

(7)

x=Ax+b或(I-A)·x=b

(8)

根据上述方程组，可求得x的唯一解，而xq0的值就是监控器中不可监控的有限序列的概率.所以，当xq0=0时，公式是可监控的；当xq0=1时，公式是弱不可监控的；当0

下面，我们将证明公式(8)中x的解的唯一性.

证明：根据马尔科夫链的性质[12,13]可知，矩阵A的特征值λ满足|λ|<1，因此，I+A+A2+…=∑n≥0An是收敛的，而：

(I-A)·(I+A+A2+…)
=(I+A+A2+A3…)-(A+A2+A3…)=I

算法 1.MPMC算法

输入：LTL公式φ

输出：公式φ的可监控性概率

1.begin

2.构造公式φ的等价监控器Mφ

4.if(U=∅)

5. return 1;

6.end if

7.if(U=Qr)

8. return 0;

9.end if

11.求解方程组的唯一解x

12.return (1-xq0)

13.end

MPMC算法的复杂度.首先，MPMC算法中构造公式φ的等价监控器Mφ的复杂度是双指数级的[6].在遍历监控器后，若集合U=∅或U=Qr，则可直接返回求解结果，无需进行后续步骤的求解，此时，算法的复杂度是O(22n)，否则，需进行线性方程组的求解，而求解方程组的时间复杂度是多项式级的，所以，算法的复杂度也是O(22n).综上，MPMC算法的复杂度是O(22n).

因此，根据x=Ax+b可列出方程组：

解上面的方程组可得：x0=13/14，x1=9/14.因此，PrM(φ2)=1-PrNM(φ2)=1-x0=1/14，即公式φ2的可监控性概率为1/14.此算法较之前的计算方法相比，避免了对无限多项进行相加的计算，表示简单，计算亦简单.

5 实验与分析

根据MPMC算法，我们设计并实现了原型系统工具monic.monic是在Linux环境下基于Spot[14]，并使用C++语言和shell脚本语言共同进行开发的，可通过命令行的方式运行.考虑到算法的性能会受到公式规模大小的影响，因此，我们利用Spot工具进行随机用例公式集合的生成.Spot工具可以通过设置LTL公式的原子命题个数及语法树大小(公式长度)来随机生成不同的公式，每个用例集合为一百个LTL公式，用例公式的参数设计如表1所示,表中的ap_nums表示原子命题个数，length表示公式的长度.本次实验的机器配置为8G内存，双核CPU，实验使用Ubuntu16.04的64位Linux操作系统，gcc 5.4.0编译器.

表1 实验用例参数Table 1 Experimental use case parameters

在monic中，概率可监控性求解器分为两种类型，其算法原理都是基于马尔可夫链的，只是一种是基于概率模型检测器PRISM[15]实现的，一种是基于SMT[16]求解器实现的，而基于SMT求解器的又可以分为基于Z3[17]和基于CVC4[18]的两种.

对于MPMC算法的三种实现，我们使用表1设计的用例集合分别对其进行了实验，实验表明MPMC算法的三种实现的求解结果是一样的.为了验证算法结果的正确性，我们使用文献[9]中的算法工具对表1设计的用例集合进行了可监控性和弱可监控性的判定求解，并根据弱不可监控公式的可监控性概率为0，可监控公式的可监控性概率为1，不可监控但弱可监控公式的可监控性概率取值范围为(0,1)的原则，通过bash脚本将MPMC算法的实验结果与可监控性和弱可监控性的判定结果进行了对比.从对比结果可以看出，所有弱不可监控的公式通过MPMC算法计算得到的可监控性概率都等于0，所有可监控的公式通过MPMC算法计算得到的可监控性概率都等于1，所有不可监控但弱可监控的公式通过MPMC算法计算得到的可监控性概率的取值范围都是(0,1).因此，我们可以判断MPMC算法的实验结果是正确的.

此外，为了对比三种实现的性能差异，我们对其进行了对比实验，实验结果如图5所示.

图5 MPMC算法的实验结果对比图Fig.5 Comparison of experimental results of MPMC algorithm

图5中x轴表示原子命题个数，y轴表示公式长度，z轴表示求解时间的对数(对数的底取10)，图中的正三角图标表示基于PRISM实现的实验结果，圆型图标表示基于Z3实现的实验结果，倒三角图标表示基于CVC4实现的实验结果.通过图中实验结果的对比，我们发现，两种基于SMT求解器实现的算法，其求解效率明显高于基于PRISM实现的算法，而基于SMT求解器实现的两种算法中，基于CVC4实现的算法的求解效率亦高于基于Z3实现的算法.这是因为基于PRISM实现的算法，其在利用PRISM进行求解的过程中，需要花费大量的时间先进行建模，然后求解；而基于SMT求解器实现的算法，由于近年来SMT求解器已经发展地相当成熟，且其无需进行复杂的建模，只需求解即可.然而值得注意的是，无论是基于PRISM实现的算法，还是基于SMT求解器实现的算法，其求解能力都是相同的，即不管求解速度如何，只要其中一种实现(不)能解得结果，其余两种都(不)能解得结果.这是因为MPMC算法是基于监控器的，因此，其都会出现随着公式规模的增大，出现监控器无法被成功构造的情况，即无法求解的情况.例如，当公式中原子命题的个数为9，公式长度为100时，对于这种情况，图中未给出求解结果.