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

• 作者: 李永明 洪云端
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 模型检测 多值可能性 Kripke结构 自动验证 模型检测器
• 年，卷（期）: 2019,（5）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 62-65,69
• 页数: 5页
• 分类号: TP393
• 字数: 3147字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2019.05.013

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李永明	陕西师范大学计算智能实验室	165	505	12.0	16.0
5	洪云端	陕西师范大学计算智能实验室	1	0	0.0	0.0