测试目的引导的模型检测方法与技术研究  

Research of model checking method and technology guided by testing purpose

作　　者：赵会群[1] 殷朝冉 

机构地区：[1]北方工业大学计算机学院

出　　处：《计算机应用研究》2015年第8期2387-2390,2394,共5页Application Research of Computers

基　　金：国家自然科学基金资助项目(61070030;61370051);北京市教委学术创新团队项目(4062012)

摘　　要：为了实现对伪代码的模型检测并且能够缓解模型检测中的状态空间爆炸问题,提出了测试目的引导的模型检测方法。该方法的基本思想是首先对伪代码进行模块划分并对每个模块进行建模,获取基本路径的集合并以流图的方式进行存储;然后利用自主开发的转换工具实现流图到国际标准语言LOTOS的转换,再利用自主开发的辅助工具μ-演算编辑器对测试目的进行描述;最后使用模型检测工具验证被测程序是否满足测试目的。实验结果表明,测试目的引导的模型检测方法能够实现对伪代码的模型检测,并且可以缓解状态空间爆炸问题。In order to realize the model Checking of pseudo code and can relieve the state space explosion problem in model checking, this paper proposed testing purpose to guide the method of model checking. First of all, it moduled partition for the pseudo code according to the ideas of layered and modeling for each module, access to the basic path set and save them in the form of flow diagrams. Then it used self-developed conversion tool to implement the transformation from the flow diagrams to the international standard language LOTOS. Secondly,it used self-developed μ-calculus editor to describe the testing purpose. Finally it used the model checking tool to verify the code under test whether it meets the testing purpose. Experimental results show that this method can realize the model checking of pseudo code and relieve the state space explosion problem in model checking.

关 键 词：模型检测 状态空间爆炸 软件测试 LOTOS μ-演算 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]