面向模型检测的Java多线程程序粗粒度自动建模方法研究

发布时间：2022-02-15 01:32

　　Java多线程程序中存在并发、同步和交互行为,导致状态爆炸,算法错误检测难度较大。调试方法和测试方法都难以覆盖并发程序全部执行路径;软件模型检测方法自动搜索并发程序全部执行路径,但在状态爆炸时难以完成。本文针对Java多线程程序提出层次着色Petri网（Hierarchical Coloured Petri Net,HCPN）粗粒度自动建模方法,在不影响模型检测结果的前提下,实现了模型及其状态空间规模缩减,有利于模型检测效率的提升。工作如下:1.提出了属性公式处理策略。粗粒度模型必须保留属性公式中待检测的状态信息,待检测状态相关的源程序语句须采用细粒度描述。因此本文提出了包含关键变量注释方法、检测相关语句自动识别方法、相关模型片段提示方法的属性公式处理策略。2.提出了包含语句粗细粒度判定功能的程序预处理方法。以语句为单位读取源程序,为每个函数构建语句二叉树,依据本文提出的粒度判定策略实现源程序语句粒度判定并标注。3.提出了细粒度和粗粒度模型描述方法。源程序中函数映射为模型页面,语句则根据类型分别映射为不同的模型片段。针对并发、同步、交互、检测相关语句等特定语句,采用细粒度描述,将一条语... 

【文章来源】：内蒙古大学内蒙古自治区211工程院校

【文章页数】：65 页

【学位级别】：硕士

【部分图文】：

类表结构

内蒙古大学硕士学位论文图 3.6(a)中的代码段除括号、变量注释外共包括 6 条语句，分别按序号对应图 3.6(b)中语句二叉树中的 6 个结点，该代码段的 if_else 结构中分别嵌套两个顺序结构。语句 2 与语句 1之间为嵌套关系，语句 2 与语句 3 之间为顺序关系，因此结点 2 作为结点 1 的左子结点，结点3 作为结点 2 的右子结点。语句 1 与语句 4 为顺序关系，因此结点 4 作为结点 1 的右子结点，语句 4、5、6 同理。语句 1 为 if 语句，对应结点 1 的 Type 属性为 if，语句 4 为 else 语句，对应结点 4 的 Type 属性为 else；语句 2、3、5、6 均为赋值语句，因此对应结点 2、3、4、5 的Type 属性值为 assignment。

VarList结构

【参考文献】：
期刊论文
[1]一种面向CPS的控制应用程序协同验证方法[J]. 张雨,董云卫,冯文龙,黄梦醒.  软件学报. 2017(05)
[2]基于CEGAR的C程序空指针解引用检测[J]. 段钊,田聪,段振华.  计算机研究与发展. 2016(01)
[3]软件模型检测中的抽象模型研究综述[J]. 魏欧,石玉峰,徐丙凤,黄志球,陈哲.  计算机研究与发展. 2015(07)
[4]基于CEGAR的Web应用验证[J]. 高洪皓,缪淮扣,曾红卫.  计算机学报. 2014(04)
[5]基于SMT求解器的路径敏感程序验证[J]. 何炎祥,吴伟,陈勇,徐超.  软件学报. 2012(10)
[6]程序代码中隐含数据与控制的Petri网建模技术[J]. 周国富,杜卓敏.  软件学报. 2011(12)
[7]一种基于认知模型检测的Web服务组合验证方法[J]. 骆翔宇,谭征,苏开乐,吴立军.  计算机学报. 2011(06)
[8]面向源代码的软件模型检测及其实现[J]. 何恺铎,顾明,宋晓宇,李力,李江.  计算机科学. 2009(01)
[9]基于抽象-验证-细化范例的软件模型检测[J]. 刘吉锋,孙吉贵.  计算机科学. 2006(12)
[10]软件模型检测中的抽象[J]. 袁志斌,徐正权,王能超.  计算机科学. 2006(07)

硕士论文
[1]基于LTL的并行软件系统CPN模型启发式模型检测方法研究[D]. 任海芬.内蒙古大学 2018
[2]单函数Java程序到CPN模型转换工具的设计与实现[D]. 霍明倩.内蒙古大学 2018
[3]FPGA程序的形式化建模与分析方法研究[D]. 陈珑.华侨大学 2015
[4]模型检测在软件方面的应用[D]. 黎吾平.吉林大学 2008



本文编号：3625643