多值可能性模型检测器的设计与实现

来源：计算机技术与发展杂志2019年第05期北京时间：

作者：洪云端;';李永明;'

摘要：随着现代计算机软件和硬件的复杂性变大,模型检测作为一种形式化自动验证技术,与传统的检测技术相比有着一系列的优势,比如可以在系统实现之前对系统进行验证,可以提前发现问题,节约大量成本。 传统的模型检测器大多是基于经典的模型检测技术实现的,而现实生活中存在大量的不确定信息,使用传统的模型检测无法解决这些问题。 而多值模型检测理论的出现,结合多值计算树逻辑,构建多值可能性 Kripke 结构模型,可以很好地解决这些问题。 为了实现模型检测自动化特性的最大优势,基于多值可能性定量模型检测的理论,设计了多值 Kripke 结构在计算机中的存储结构、计算模块等,实现了一个基于多值可能性测度的多值计算树逻辑的模型检测器 MvChecker,使得用户可以自动验证系统性质。

关键词：模型检测;多值可能性;Kripke结构;自动验证;模型检测器