软件运行时验证加速中的多目标约束模型研究

刘彦斌,叶 飞，王毅刚

(1.中国电子科技集团公司第十三研究所，石家庄 050051；

2.中国人民解放军军械工程学院，石家庄 050003)



【信息科学与控制工程】

软件运行时验证加速中的多目标约束模型研究

刘彦斌1,叶 飞2，王毅刚2

(1.中国电子科技集团公司第十三研究所，石家庄 050051；

2.中国人民解放军军械工程学院，石家庄 050003)

由于复杂性质的运行时验证中常产生高额时间开销，影响了该技术在系统部署后的应用；减小验证开销提高验证效率已成为亟待解决的难点问题；通过识别运行时验证优化过程中多目标约束间的内在依赖关系，定义并构建了可加速监控器的判定方程，作为验证加速中的多目标约束模型；实验表明：该模型的求解结果能够用来判定可加速监控器，为实施软件运行时验证加速提供量化依据。

运行时验证；多目标约束；监控器；监控开销；运行时监控

运行时验证(Runtime Verification)是一种近10多年来逐步兴起的针对程序具体运行的轻量级验证技术[1]。它把形式化验证技术和系统的实际运行结合起来，通过监控程序运行并检验其是否满足给定性质实现对系统的验证。由于运行时验证针对的对象仅仅是系统运行中的单个或者少数执行轨迹，不需针对整个系统模型，避免了状态空间爆炸。但是，参数化性质等较为复杂性质的在线运行时验证中，由于需要维持大量的监控器实例并处理程序实体中生成的大量事件，经常产生高额的时间开销。研究表明：当前具有代表性的运行时验证工具JavaMOP[2]和Tracematches[3]所产生的平均开销分别为41%和112%，如此高的开销，是用户所不能容忍的。开销问题阻碍了运行时验证技术在实践中广泛用于软件部署后环境。减小软件运行时验证开销，已成为当前亟待解决的难点问题。

由于性质验证和诊断所需信息源可能部分重叠，在开销优化过程中不仅影响系统验证结果的准确性，而且可能影响诊断所需信息的收集，即对诊断支持能力造成潜在不良影响。因此，把软件运行时验证加速归结为多目标优化问题，不仅需要将开销做为优化目标，还需考虑开销优化对验证结果准确性以及诊断支持能力的影响。软件运行时验证加速过程需要在减小监控开销、提高验证精度和改善诊断支持能力多个互相制约的目标间进行权衡。建立多目标约束模型，并基于该模型确定优化对象，是实施软件运行时验证加速首先需要解决的问题。

本文通过识别运行时验证优化过程中多目标约束间的内在依赖关系，通过量化分析运行时验证加速中的多目标约束，包括性质违背检测能力、监控开销评估、诊断支持能力以及监控器优化的正确性，在此基础上构建了可加速监控器的判定方程，作为运行时验证加速的多目标约束模型。该多目标约束模型的求解结果可判定“可加速”的监控器，为实施软件运行时验证加速提供依据。

1 研究现状

当前针对软件运行时验证加速的研究主要包括以下几类：

1) 联合静态分析减小开销。Bodden等[4]探索了许多轻量级的代码静态分析方法，通过识别可安全移除的插桩点减小开销。Purandare 等[5]优化了程序中性质相关的循环结构，通过仅仅监控有限次数的循环减小开销。

2) 基于周期性取样的开销优化方法。Bonakdarpour等[6]提出了时间触发的运行时验证概念，监控器周期性地程序状态取样来评估性质是否成立。Navabpour等[7]研究了采用启发式算法求解给定取样周期内需要被缓冲的最小数量的关键事件，以便时间-触发的监控器能够成功重构两个连续取样时间内的程序状态[8]，优化取样周期最小化所需外存储器，以便监控器能够正确地恢复程序状态变化序列。

3) 基于控制理论的解决方案[9]。针对CPS系统，提出新的基于控制理论的软件监控解决方案来协调可预测性以及内存利用率。

4) 基于并行运行监控器减小开销[10]。例如，通过在GPU中运行监控器实现监控和功能进程的分离，并行监控并验证程序。针对基于的系统，通过将不同组件运行在不同的计算机核中，减小运行时验证开销[11]。

但上述研究单纯考虑如何减小运行时验证开销，没有把软件运行时验证加速归结为多目标优化问题。

2 多目标决策基本原理

多目标决策与单目标决策不同，其最显著特点是目标之间的不可公度性和目标产生的矛盾性。因此，单目标决策问题具有最优解，多目标决策问题通常无法找到最优解。多目标决策中，一般不存在所有目标函数共同的极大值点，通常求取其非劣解或最优解[12]。多目标决策的标准形式是:

(VOP) max[f1(x),f2(x),…,fp(x)]

s.t.x∈X

其中，X=(x1,x2,…xn)T是n维向量，x所在的空间叫决策空间；f1(x),f2(x),…,fn(x)为目标函数，p维向量(f1(x),f2(x),…,fp(x))所在空间称为目标空间；X是决策空间上的可行集。多目标决策过程就是求解得到近似的非劣解集的过程。

本文将监控器标识为m，所对应的监控器集合m=(m1,m2,…,mn)T是N维向量,m所在的空间是决策空间。m对应的目标函数分别标识为f1(m)，f2(m)和f3(m)，其中：f1(m)为性质违背检测能力评估函数;f2(m)为监控开销量化评估函数;f3(m)为诊断支持能力评估函数。

三维向量(f1(m)，f2(m)和f3(m))所在空间是目标空间。针对具体的软件系统，需要在多目标约束下求解得到决策空间上的最优解M，将M中的监控器转换插入目标软件，对其进行运行时监控。

3 多目标约束分析

3.1 性质违背检测能力

从运行时验证角度而言，并非程序执行中所有的性质都能够被监测。LamportL最早将反应式系统的性质分为安全性和活性两大类[13]，简单而言，安全性意味着“一些坏的事情在程序执行期间从来不会发生”，而活性意味着“一些好的事情将最终发生”。

由于运行监测器仅仅能够观察有限的执行步骤，而活性需要通过无限序列行为决定，通常是不可监测的。对于反应式系统而言，只有把活性转换成有限时间区间的行为(如系统必须在固定的时间限制内响应请求)才能进行监测，而安全性质一般是可以监测的。但是，安全性质未必都是可监测的性质(如图灵机停机问题的安全关闭，是安全性质，但由于不可判定，从而是不可监测的性质)。因此，可以得出结论，可监测的性质是安全性质的真子集[14]。

对于σ∈Sw，用pref(σ)作为σ的所有有限前缀的集合，则可监测的性质可以定义如下：

由于监测器能够监测的仅仅是安全性质的子集，因此只有那些能够被监测器在有限轨迹内识别的性质才能作为监测需求规约。同时，在可监测的性质当中，并非所有性质都是需要进行监测的。为减少监测对系统带来的额外开销，如占用系统资源，影响软件执行时间等，应尽可能减少被监测的性质数量。

3.2 监控开销评估

本文中的开销是指时间开销，是对在运行时验证中由于监控程序需要额外执行的时间的度量。如果最初程序执行时间为R，插桩后伴有监控的程序执行时间为R+K，则监控开销是K/R。

监控开销量化评估函数f2(m)=K/R,其中，K=y(x1,x2,…,xK),K的大小和多个因素相关，是被监控变量的数量、位置、监控需求描述语言、验证算法等因素的函数。通过尽可能减小被监测的性质及变量的数量，并对监控需求描述语言中逻辑算子的形式和数量进行限制等途径，可以减小监控开销。

首先，为减少被监控变量的数量，选取监测需求规约，需要遵循以下原则：选取“可监测的”性质；选取那些“可疑的”无法通过常规软件测试进行确认的性质进行监测；根据失效引起的危害程度，优先选取“严酷度”高的性质进行监测；根据目标软件特点及对开销的容忍程度，选取被监测的性质数目。

其次，一般说来，采用过去时间LTL或者MTL书写的公式比采用将来时间的公式更容易表达安全性需求。由于这些公式仅仅涉及过去，它们的值在轨迹中的任何状态中通常或者为True或者为False，而不像将来时间公式那样，需要在“未来”进行判定。从而这些过去时间书写的性质规约更适于基于逻辑的监测。因此，在监测需求规约生成中尽可能采用过去时间算子进行性质表达。

第三，由于在监测中，每个算子都将占用额外的内存，为了尽可能缩小监测开销，需要简化给定逻辑中算子的数量。利用算子之间的等价关系，可以对算子进行简化。例如，对于过去时间LTL，采用监测算子{↑,↓,[ )s}可表达所有的标准过去时间LTL算子φ|◆φ|φ|φSsψ|φSwψ。从而，可把采用标准过去算子生成的公式转化为采用监测算子{↑,↓,[ )s}表示的性质规约，减小验证开销。

3.3 监控器优化的正确性

程序可看作由许多在不同的状态下具有不同取值的程序变量组成，所有程序变量的某一次取值称之为系统的一个状态，从而，一个典型的程序执行模型可看作是一个又一个状态所组成的序列：

定义2：执行：程序执行是一个无限状态序列σ=s0,s1, …，si∈S，S是状态的集合；程序执行轨迹π[i，j]表示π从状态si到状态sj的子序列si,si+1,…,sj。

软件行为是执行的集合，软件性质(Property)是期望的软件行为的描述，即执行中那些(无限)状态序列所满足的性质。性质反映了状态内部和状态之间的关系，回答了状态的什么关系导致软件可接受的外部行为(即软件需求)的问题。

定义3：监控器优化的正确性：对于性质∅和未优化的监控器M，符合下列条件时称M被正确优化：对于每个轨迹π，监控器M观察得到π′，且|π′|≤|π|；M观察到π发生性质违背时，M′都能报告π′发生性质违背。

3.4 诊断支持能力

根据GJB3385—98，术语“诊断”是指检测故障和隔离故障的过程。它的实质是从征兆出发，通过信息的处理，正确地确定故障原因、类型和位置。由于软件故障具有随机性，软件故障状态随着程序执行的结束而消失并且难以进行重现，等到系统失效发生后，再去进行故障诊断常常“为时已晚”，常常很难断定失效究竟是软件故障还是硬件故障，从而需要根据故障监测信息进行故障诊断。同时，为减小软件运行监测给系统带来的开销，监测能够从软件运行中提取的信息需尽可能的少。也就是说，软件运行监测必须“精确”地捕获能够作为征兆的故障信息。

由于部署后应用系统中的软件一般经过了大量的软件测试，包括静态测试、动态测试等。残留的软件故障最可能的是逻辑和时序约束方面的故障以及和硬件接口的输入/输出故障，因为这些故障和真实运行环境有关，只有在某些特殊情况下才可能出现，常规的软件测试难以发现。因此，需要对这些方面的特性进行监测，主要包括功能特性、时序性质以及时间约束。主要采用LTL和MTL，根据这几方面特性，提取监测需求公式；并在系统运行期间运行验证这些公式是否发生性质违背，发生性质违背时的故障体现为上述3个方面，发现性质违背时能够用来揭示故障原因的软件运行状态被称作诊断信息D。

定义4：监控器优化中的诊断信息保持：对于性质∅，未优化的监控器M，M观察到的轨迹为π，诊断信息为D；对于优化过的监控器M′，如果监控器M′观察得到的每个轨迹π′，都满足D∩π=D∩π′，则称优化后的监控器保持了诊断信息,此时诊断支持能力评估函数f3(M)=f3(M′)。

4 多目标约束模型的构建

在实施运行时验证加速之前，需要首先判定出哪些监控器是“可加速”的，即判定出哪些监控器在运行中不再必要、哪些可以进行动态调整，且满足多目标约束。因此，需要构建可加速监控器的判定方程。

定义5：单个可加速监控器：对于某监控器m而言,如存在对其优化后的监控器m′，满足下列条件：性质违背检测能力评估函数f1(m)=f1(m′)，监控开销量化评估函数f2(m)>f2(m′),诊断支持能力评估函数f3(m)=f3(m′)，则称m为可加速监控器m，加速后的监控器为m′。

定义6：可加速监控器组：对于监控器M=(m1,m2,…,mn)，如果M中存在监控器组L=(mi,mj,…,mk)，使得对L优化后的监控器，满足下列条件：性质违背检测能力评估函数f1(L)≤f1(L′)，监控开销量化评估函数f2(L)>f2(L′)，诊断支持能力评估函数f3(L)≤f3(L′)，则称L为可加速监控器组。

本项目所说的可加速监控器既包括单个可加速监控器，也包括可加速监控器组，是对两者的统称。软件运行时验证加速过程需要在减小监控开销、提高验证精度和改善诊断支持能力多个互相制约的目标间进行权衡，对可加速监控器的判定过程定义如下。

定义7：可加速监控器的判定：对监控器M=(m1,m2,…,mn)中的可加速监控器进行判定的过程，就是求解下列约束方程Cmul得到监控器M′的过程：

利用性质的语义结构分析和从程序运行中获得的执行轨迹等监控信息，已构建了启发式算法对该多目标约束方程Cmul进行求解。实验表明，该方程的求解结果能够有效判定出哪些监控器是“可加速”的，为实施软件运行时验证加速提供量化依据。

5 实验验证

为了验证上述模型，采用某卫星控制系统作为案例开展实验。该卫星载有多种执行各种任务的设备(如照相机、温度传感器等)，地面人员通过操作指令可对卫星进行控制。卫星上发生的每个重要事件都被记录在日志中并传回给地面，地面日志模块接受并存储这些事件。我们将通过这些数据对软件进行运行时验证。

在实验环境下，采用受控实验方法收集其加速前完整的程序执行轨迹信息，共生成500个轨迹，每个轨迹包含400个命令，平均轨迹长度是2 000个事件。此外，还收集了监控开销、验证精度、诊断支持能力相关的实验数据。

在验证加速前，选取了CommandSuccess等各类不同类型的性质作为待验证性质，系统中总共包含12个监控器M=(m1,m2,…,m12)。例如，该卫星系统期望行为应满足命令成功(CommandSuccess)性质：每个Command(i,n,t1)事件应当最终跟随Suceess(i,n,t2)事件，在期间不能有Fail(i,n,t3)事件发生。该性质可以用LTL表达如下：

□(Command(i,n,_)⟹Fail(i,n,_)USuccsee(i,n,_))

其中，□含义是“always”,U含义是”until”。

根据所收集实验数据，结合定性评估和定量分析方法，得到了多目标约束模型Cmul的具体参数。接着，通过启发式迭代算法对多目标模型求解，判定出性质L=(m2,m8,m10,m11)为可加速监控器组，其中m2在运行中不再必要，m8、m11可进行动态调整，m10可改为以某时间间隔取样验证模式，且满足多目标约束。根据该结果，将优化后的监控器转换插入目标软件实施运行时验证。

通过对比加速前后的实验数据，结果表明，所构建模型的求解结果能够作为实施软件运行时验证加速的依据。在加速前平均开销为51%，加速之后在满足验证精度、诊断支持能力前提下平均开销减小为28%。

6 结束语

本文从多目标优化角度研究软件运行时验证的加速问题，通过量化运行时验证的多目标约束，构建了可加速监控器的判定方程，作为运行时验证加速的多目标约束模型。实验表明：该模型的求解结果能够为实施软件运行时验证加速提供量化依据。下一步，我们将继续优化本文所构建的多目标约束模型并改进对该模型求解的启发式算法。

[1] FALCONE Y,FERNANDEZ J C,MOUNIER L.What can you verify and enforce at runtime[J].International Journal on Software Tools for Technology Transfer,2012,14(3):349-382.

[2] BODDEN E.Collaborative Runtime Verification with Tracematches[J].Journal of Logic and Computation,2010,20(3):707-723.

[3] CHEN F,ROSU G.MOP:An Efficient and Generic Runtime Verification Framework[J].Acm Sigplan Notices,2007,42(10):569-588.

[4] BODDEN E.Efficient Hybrid Typestate Analysis by Determining Continuation-Equivalent States[C]//Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering,2010.

[5] PURANDARE R,DWYER M B,ELBAUM S.Monitor Optimization Via Stutter-equivalent Loop Transformation[C]//Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications,2010.

[6] BONAKDARPOUR B,NAVABPOUR S,FISCHMEISTER S.Sampling-based Runtime Verification[C]//Proceedings of the 17th International Conference on Formal Methods，2011.

[7] NAVABPOUR S,WU C W W,BONAKDARPOUR B,et al.Efficient Techniques for Near-Optimal Instrumentation in Time-Triggered Runtime Verification[C]//Runtime Verification.Springer Berlin Heidelberg,2011:208-222.[8] BONAKDARPOUR B,NAVABPOUR S,FISCHMEISTER S.Form Methods Syst Des,2013,43:29.

[9] MEDHAT R,BONAKDARPOUR B,KUMAR D,et al.Runtime Monitoring of Cyber-Physical Systems Under Timing and Memory Constraints[J].ACM Transactions on Embedded Computing Systems (TECS),2015,14(4):79.

[10]BERKOVICH S,BONAKDARPOUR B,FISCHMEISTER S.GPU-based Runtime Verification[J].IEEE International Parallel & Distributed Processing Symposium (IPDPS),2013(5).

[11]NAVABPOUR S,BONAKDARPOUR B,FISCHMEISTER S.Time-Triggered Runtime Verification of Component-Based Multi-core Systems[C]//Runtime Verification，2015:153-168.

[12]周佳.支持故障恢复的多目标约束路由算法研究[D].北京：解放军信息工程大学,2010.

[13]DWYER M B,PURANDARE R,PERSON S.Runtime Verification in Context:can Optimizing Error Detection Improve Fault Diagnosis[C]//Proceedings of the First International Conference on Runtime Verification,2010.

[14]VISWANATHAN M,KANNAN S,LEE I.Foundations for the Run-time Analysis of Software Systems[J].2000.

[15]冉慧，宋雪. 求解约束优化问题的无参数填充函数算法[J].重庆理工大学学报(自然科学)，2013(5)：132-136.

(责任编辑 杨继森)

Research on Modeling for Multi-Objective Constraint Among Speeding up Runtime Verification

LIU Yan-bin1, YE Fei2, WANG Yi-gang2

(1.The No. 13rdResearch Institute of China Electronics Technology Group Corporation, Shijiazhuang 050051, China; 2.Ordnance Engineering College of PLA, Shijiazhuang 050003, China)

Runtime verification of complicated properties imposed high overhead, which influences us to apply this method in the context of deployed systems. By identifying inherent dependencies among multi-objective constraint of runtime verification, a decision equation was constructed to decide that which is optimizable monitor, and this decision equation can be considered as a multi-objective constrained model for speeding up runtime verification. Experimental results show that this model is capable of deciding that the optimizable monitor and provides a quantitative basis for speeding up runtime verification.

runtime verification; multi-objective constraint; monitor; monitoring overhead; runtime monitoring

2016-03-12；

2016-05-15

河北省自然科学基金项目(F2014506017)

刘彦斌(1978—)，男，博士，主要从事可信软件研究。

10.11809/scbgxb2016.10.016

刘彦斌,叶飞，王毅刚.软件运行时验证加速中的多目标约束模型研究[J].兵器装备工程学报，2016(10):80-83.

format:LIU Yan-bin,YE Fei,WANG Yi-gang.Research on Modeling for Multi-Objective Constraint Among Speeding up Runtime Verification[J].Journal of Ordnance Equipment Engineering,2016(10):80-83.

TP311

A

2096-2304(2016)10-0080-05