符号模型检测的研究

发布时间：2020-06-16 10:55

【摘要】： 计算机软硬件系统日益复杂,在很多系统中,测试、模拟等传统的验证方法已不能保证其正确性和可靠性。模型检测技术产生于上世纪80年代,由美国的Clarke和Emerson,法国的Quielle和Sifakis分别独立提出。在该形式化验证方法中,系统性质用命题时态逻辑公式表示,有限状态反应系统(硬件电路、通讯协议)用状态转换系统描述,有效的查询过程检测模型,判断模型是否满足系统性质。然而,随着系统规模的增大,状态数呈指数上升的状况和显式模型检测有限的处理能力之间存在难以克服的矛盾,即状态爆炸。1986年,Bryant将传统的二值判定图BDD技术加以改进,使之成为布尔函数的规范表示方法。之后McMillan将这种技术应用于模型检测中,基于BDD的模型检测称为符号模型检测。符号模型检测的主要特点是用BDD隐式地表示有限状态反应系统的状态集合和状态转换集合,空间爆炸问题被有效缓解。 本研究实现了一个基本的符号模型检测器CTLMC。该模型检测器直接采用布尔函数作为系统模型的描述语言,用来描述模型的初始状态集合和系统状态转换关系;采用CTL时态逻辑作为系统性质的描述语言,用来描述系统应该满足的需求(性质);采用CTL符号模型检测算法计算模型是否满足性质。 此外,在实现CTLMC过程中发现一种基于BDD的SMC中PRE(?)操作的改进算法,该算法处理PRE(?)步骤3(嵌套布尔存在量化)的方法是,一次遍历“删除”所有被量化变量的节点,产生表示布尔函数与嵌套存在量化结果等价的不确定排序二值判定图,然后把不确定排序二值判定图转换成OBDD。实验表明该算法能有效缩短计算时间,减少中间节点所需空间。
【学位授予单位】：西安理工大学
【学位级别】：硕士
【学位授予年份】：2008
【分类号】：TP306
【图文】：

黝黝黝翼翼濒濒 MMM满足 sssssM不满足 sss图1一 2CTLMC结构概图Fig.l一 2CTLMCframework.6论文的组织结构论文的后续章节分别为:第二章系统模型，主要介绍系统模型的表示，如何用脸ipke状态转换图和布尔函数表示，以及布尔函数词法语法解析器的实现，最后介绍二值判定图和布尔函数对应的二值判定图的生成算法。第三章系统性质，主要介绍计算树时态逻辑CTL和CTL词法语法解析器的实现。第四章模型检测，主要介绍Labeling检测算法和cTLMc所采用的符号模型检测算法。

芍芍勺勺【【)已 已已}积 积 芍芍口口 lll刁，，，，，， 芍芍口口【【〕日日 图1一 3CTLMC界面Fig.1一 3CnJMCuserinterface

【引证文献】

相关期刊论文 前1条

1 韩树森;戴航;;模型检验下蠕虫病毒检测器的设计与实现[J];现代电子技术;2012年03期

相关硕士学位论文 前4条

1 于帅帅;基于RPR的核电数字化保护系统安全通信网络的研究[D];上海交通大学;2011年

2 闻晓;一种基于Mealy机的BPEL程序验证模型研究[D];西南大学;2009年

3 高超;安全级软件验证与确认中测试技术研究[D];上海交通大学;2010年

4 张泽恩;基于GSTE中的符号仿真设计与实现[D];电子科技大学;2012年

本文编号：2715956