基于动态执行的程序时序性质验证

发布时间：2022-02-11 19:03

　　为了提高大规模软件系统的可靠性和安全性,程序的形式化验证受到广泛关注。传统模型检测方法需要从源代码中提取模型,然而,随着程序规模增大以及结构的复杂化,从程序中提取模型变得异常困难,任何一个错误都可能造成模型和源程序的不一致。近年来,源代码级别的形式化验证已成为一个重要的研究课题。其研究主要分为以下三个方向:第一,可达性分析方法,该方法在待验证程序中插桩错误标签,然后通过分析错误标签的可达性来验证程序是否满足指定性质,然而该方法仅能进行安全性验证,而无法验证诸如活性的其他时序性质。第二,静态软件模型检测方法,该方法不执行程序,静态检测程序所有路径,从而使得较小规模程序都可能产生很大的状态空间,因此很难验证大规模程序,且验证效率不高。而且由于没有程序的执行信息,导致精确性不够,可能产生误报。第三,运行时验证方法,在执行程序时提取事件信息,构造监控器来检测当前的执行路径是否满足指定性质,由于每次只验证一条路径,避免了状态空间爆炸问题。尽管在代码级别程序验证方面已有一些研究工作,然而现有技术并不成熟,现有验证工具仍无法处理大规模应用程序。本文围绕代码级别的形式化验证方法进行研究,主要工作如下:... 

【文章来源】：西安电子科技大学陕西省211工程院校教育部直属院校

【文章页数】：156 页

【学位级别】：博士

【部分图文】：

运行时验证框架

这里的<==即为MSVL语句中的赋值操作，编写程序时，由于编译器无法识别特殊字符 ，我们用<==替代 。如图3.2所示，图左边是LNFG，右边是由它生成的MSVL程序。因为只有一个fin标记 1出现在节点2中，所以我们将它存储在集合 2= { 1}中。最初，初始节点集合被转为程序CuNode <== 1 or CuNode <== 2。对于节点1，从1到3的边转换成if( ) then{CuNode := 3}else{false}，从1到4的边转换成if(true)then{CuNode :=4}else {false}，等价为CuNode := 4。于是有 1=“if( )then{CuNode := 3}else{false}38

′ 在执行该程序时，可以获取到一个如图3.5(a)所示的无穷的无环路径 = 0, 1, 2, 3, 4, 5, ... 。 然而，我们可以从中抽象出一个有环的简化计算 ( ) = 0, 1, 2,47

【参考文献】：
期刊论文
[1]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明.  软件学报. 2019(01)
[2]Model checking concurrent systems with MSVL[J]. Nan ZHANG,Zhenhua DUAN,Cong TIAN.  Science China（Information Sciences）. 2016(11)
[3]运行时验证技术的研究进展[J]. 张硕,贺飞.  计算机科学. 2014(S2)



本文编号：3620796