中文摘要：

为了实现对伪代码的模型检测并且能够缓解模型检测中的状态空间爆炸问题,提出了测试目的引导的模型检测方法。该方法的基本思想是首先对伪代码进行模块划分并对每个模块进行建模,获取基本路径的集合并以流图的方式进行存储;然后利用自主开发的转换工具实现流图到国际标准语言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.