«上一篇/Previous Article|本期目录/Table of Contents|下一篇/Next Article»

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:

29

期数:

2019年05期

页码:

62-65

栏目:

智能、算法、系统工程

出版日期:

2019-05-10

文章信息/Info

Title:

Design and Realization of Multi-valued Model Checker

文章编号:

1673-629X(2019)05-0062-04

作者:

洪云端¹; 2; 李永明¹; 2

1. 陕西师范大学 计算智能实验室,陕西 西安 710119;2. 陕西师范大学 计算机科学学院,陕西 西安 710119

Author(s):

HONG Yun-duan¹; 2; LI Yong-ming¹; 2

1. Computational Intelligence Laboratory,Shaanxi Normal University,Xi’an 710119,China;2. School of Computer Science,Shaanxi Normal University,Xi’an 710119,China

关键词:

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

Keywords:

model checking; multi-valued possibility; Kripke structure; automatic verification; model checker

分类号:

TP393

DOI:

10. 3969 / j. issn. 1673-629X. 2019. 05. 013

摘要:

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

Abstract:

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 multivalued model theory,combined with multi-value computation tree logic to construct multi-value possibilistic Kripke model that can be aneffective solution to these problems. In order to achieve the advantage of automatic characteristics of the model checking,based on thetheory of multi-valued possibility quantitative model checking,we design the storage structure and calculation module of multi-valueKripke structure in computer,and implements a model detector MvChecker based on multi-valued possibility measure of multi-valuedcalculation tree logic,so that users can automatically verify the system property

常用功能

更新日期/Last Update: 2019-05-10