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

Design and Realization of Multi-valued Model Checker

作　　者：洪云端 李永明[1,2] HONG Yun-duan;LI Yong-ming(Computational Intelligence Laboratory,Shaanxi Normal University,Xi’an 710119,China;School of Computer Science,Shaanxi Normal University,Xi’an 710119,China)

机构地区：[1]陕西师范大学计算智能实验室,陕西西安710119 [2]陕西师范大学计算机科学学院,陕西西安710119

出　　处：《计算机技术与发展》2019年第5期62-65,69,共5页Computer Technology and Development

基　　金：国家自然科学基金(11671244)

摘　　要：随着现代计算机软件和硬件的复杂性变大,模型检测作为一种形式化自动验证技术,与传统的检测技术相比有着一系列的优势,比如可以在系统实现之前对系统进行验证,可以提前发现问题,节约大量成本。传统的模型检测器大多是基于经典的模型检测技术实现的,而现实生活中存在大量的不确定信息,使用传统的模型检测无法解决这些问题。而多值模型检测理论的出现,结合多值计算树逻辑,构建多值可能性Kripke结构模型,可以很好地解决这些问题。为了实现模型检测自动化特性的最大优势,基于多值可能性定量模型检测的理论,设计了多值Kripke结构在计算机中的存储结构、计算模块等,实现了一个基于多值可能性测度的多值计算树逻辑的模型检测器MvChecker,使得用户可以自动验证系统性质。With the increasing complexity of modern computer software and hardware,model detection,as a formalized automatic verification technology,has a series of advantages over traditional detection technology. For example,it can verify the system before the system implementation,detect problems in advance,and save a lot of costs. The traditional model checker is mostly based on the classic theory of model checking,but in real life there are a lot of uncertain information,so it cannot solve these problems. For this,we use multi-valued model theory,combined with multi-value computation tree logic to construct multi-value possibilistic Kripke model that can be an effective solution to these problems. In order to achieve the advantage of automatic characteristics of the model checking,based on the theory of multi-valued possibility quantitative model checking,we design the storage structure and calculation module of multi-value Kripke structure in computer,and implements a model detector MvChecker based on multi-valued possibility measure of multi-valued calculation tree logic,so that users can automatically verify the system property。

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术]