程序模型检测的两阶段框架

摘要

模型检测是一种对有限状态变迁系统验证其时态逻辑性质的重要方法,可以弥补测试技术的不足.基于流分析的程序模型检测和基于语言转换的程序模型检测是当前程序模型检测的主要方法,它们都存在各自的局限性.基于对这两种程序模型检测方法各自优缺点的分析,提出了一种两阶段程序模型检测框架,通过结合两种程序模型检测方法,可有效提高程序模型检测对较大规模程序的适用性.