论文研究-测试目的引导的模型检测方法与技术研究.pdf

为了实现对伪代码的模型检测并且能够缓解模型检测中的状态空间爆炸问题，提出了测试目的引导的模型检测方法。该方法的基本思想是首先对伪代码进行模块划分并对每个模块进行建模，获取基本路径的集合并以流图的方式进行存储；然后利用自主开发的转换工具实现流图到国际标准语言LOTOS的转换，再利用自主开发的辅助工具μ-演算编辑器对测试目的进行描述；最后使用模型检测工具验证被测程序是否满足测试目的。实验结果表明，测试目的引导的模型检测方法能够实现对伪代码的模型检测，并且可以缓解状态空间爆炸问题。