测试目的引导的模型检测方法与技术研究
为了解决模型检测中的状态空间爆炸问题,提出了测试目的引导的模型检测方法.该方法的基本思想是首先在伪代码的层次上根据分层思想对被测系统进行模块划分并对每个模块进行建模,获取基本路径的集合并以流图的方式进行存储.然后利用自主开发的转换工具实现被测系统到国际标准语言LOTOS的转换.其次利用自主开发的μ-演算编辑器根据测试目的选取待测属性,并使用μ-演算描述该属性.最后使用模型检测工具验证被测系统是否满足待测属性.
软件工程 模型检测 分层思想 语言转换
赵会群 殷朝冉
北方工业大学信息工程学院,北京中国100144
国内会议
武汉
中文
299-304
2014-07-19（万方平台首次上网日期，不代表论文的发表时间）