关键词:
Colored Petri Net
单函数Java程序
模型文件
CPN Tools
摘要:
目前,软件应用十分广泛,在软件开发的前期检测出错误的代价比后期发现并修改的代价要低。传统的基于模型的测试方法存在两方面的弊端,一是手工建模,模型的正确性不易保证,二是建模和测试的工作量很大,效率偏低。因此,本文设计并实现一个单函数Java程序到着色Petri网(Colored Petri Net,CPN)模型的转换工具。通过读入待测程序,自动分析处理并导出完全符合CPN Tools格式的模型文件。一方面,生成CPN模型的过程实现了自动化,提升建模效率;另一方面,本工具不是针对软件需求建模,而是直接针对代码实现建模,自动导出了符合CPN Tools格式的模型文件,可进一步使用CPN模型检测技术发现模型的错误,从而直接发现代码中的算法错误。本文完成了如下工作:(1)读入待测程序:对单函数Java待测程序进行读入、分析及存储处理。其中声明语句采用链表存储,其他语句采用二叉树存储,通过树中结点的左右子树区分后续语句的嵌套关系。(2)转换待测程序:对程序中的变量定义、流程控制及操作处理等分析,完成程序到CPN模型的转换。其中,程序中定义的变量转换为模型中的token流转,通过颜色集和变量组完成;程序中全部处理语句转换为CPN模型,通过模型元素完成,包括位置、变迁、弧、变迁防卫表达式、弧表达式等。(3)生成模型文件:根据CPN Tools模型文件格式生成并导出模型文件。导出的模型文件可直接由标准CPN Tools打开,用于基于模型检测的算法错误发现。最后,通过实例应用及执行效果分析,说明本文实现的单函数Java程序到CPN模型转换工具能够自动完成针对程序的建模工作,能够提升建模效率,有利于下一步通过模型检查技术检查算法错误,能够在一定程度上提升软件质量。