论文部分内容阅读
Java多线程程序中存在并发、同步和交互行为,导致状态爆炸,算法错误检测难度较大。调试方法和测试方法都难以覆盖并发程序全部执行路径;软件模型检测方法自动搜索并发程序全部执行路径,但在状态爆炸时难以完成。本文针对Java多线程程序提出层次着色Petri网(Hierarchical Coloured Petri Net,HCPN)粗粒度自动建模方法,在不影响模型检测结果的前提下,实现了模型及其状态空间规模缩减,有利于模型检测效率的提升。工作如下:1.提出了属性公式处理策略。粗粒度模型必须保留属性公式中待检测的状态信息,待检测状态相关的源程序语句须采用细粒度描述。因此本文提出了包含关键变量注释方法、检测相关语句自动识别方法、相关模型片段提示方法的属性公式处理策略。2.提出了包含语句粗细粒度判定功能的程序预处理方法。以语句为单位读取源程序,为每个函数构建语句二叉树,依据本文提出的粒度判定策略实现源程序语句粒度判定并标注。3.提出了细粒度和粗粒度模型描述方法。源程序中函数映射为模型页面,语句则根据类型分别映射为不同的模型片段。针对并发、同步、交互、检测相关语句等特定语句,采用细粒度描述,将一条语句映射为一个模型片段;对其他语句采用粗粒度描述,将多条语句映射为一个模型片段,并运用复杂弧表达式实现单个模型片段与多条语句的功能等价性。4.提出了复杂弧表达式生成方法。HCPN弧表达式采用ML(Meta Language)语法规则,本文通过预定义函数模板及嵌套调用的方式,实现粗粒度模型片段中复杂弧表达式生成。特别地,源程序语句中的嵌套关系被映射为函数调用,ML语言不支持的循环被映射为函数递归调用。最后,通过实例对比分析,验证了粗粒度建模方法可有效缩减模型及其状态空间规模,且不影响模型检测结果。