形式化方法B的精化

1

作者 高洪江 覃征 +1 位作者 鹿蕾 邵利平 《计算机工程》 CAS CSCD 北大核心 2007年第9期49-51,共3页

形式化方法B支持从抽象规约到实现的完整的开发过程,用于开发安全关键的软件系统。给出了B方法精化的定义后,介绍了抽象机的精化过程与方法,结合实例分析了仅使用前向精化的普通精化规则的不完整性,通过引入反向精化提供了完备的精化理... 形式化方法B支持从抽象规约到实现的完整的开发过程,用于开发安全关键的软件系统。给出了B方法精化的定义后,介绍了抽象机的精化过程与方法,结合实例分析了仅使用前向精化的普通精化规则的不完整性,通过引入反向精化提供了完备的精化理论,二者联合起来能够证明任何正确的精化。 展开更多

关键词 形式化方法 广义代换 抽象机 前向精化 反向精化 证明义务

下载PDF 职称材料

采用CPAChecker的动态程序验证 被引量：3

2

作者 段钊 刘锟龙 《西安电子科技大学学报》 EI CAS CSCD 北大核心 2019年第1期33-38,共6页

针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法.首先,根据程序的控制流程图,对程序进行静态检测。在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检... 针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法.首先,根据程序的控制流程图,对程序进行静态检测。在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检测的过程。其中,抽象检测可以有效地限制系统模型的规模,动态执行不仅可以有效地减少静态检测导致的误判,而且有助于引导构建精确的系统模型,降低虚假反例的数量和不必要的反例分析和精化。实验数据显示,这种算法明显提高了传统的反例引导谓词抽象精化算法的检测效率和准确率。 展开更多

关键词 模型检测 抽象精化 动态执行 程序验证 状态空间爆炸

下载PDF 职称材料

一个抽象机库中B方法的研究 被引量：1

3

作者 杨丹 梁洪峻 《微计算机应用》 2007年第10期1117-1120,共4页

B方法是支持规格说明到软件设计和执行的形式化方法。文章研究了B方法中一种抽象机库的实现模型和生成代码,对该方法的特点进行评述。验证了B的正确可靠的实现方法,充分利用B方法的精化原则,提高了B形式化方法的开发验证效率。

关键词 B方法 抽象机 精化 证明义务

下载PDF 职称材料

B方法规格说明的构造及应用 被引量：1

4

作者 吴帅 杨庆红 樊艳芬 《计算机与现代化》 2007年第5期29-32,35,共5页

B方法是一种软件形式化方法,支持从规格说明到代码生成的整个软件开发周期。本文比较系统地分析了B方法规格说明的构造结构,并结合所设计的实例演示了用B方法编写规格说明的过程,简略地给出了其规格说明的证明义务,并对其规格说明进行... B方法是一种软件形式化方法,支持从规格说明到代码生成的整个软件开发周期。本文比较系统地分析了B方法规格说明的构造结构,并结合所设计的实例演示了用B方法编写规格说明的过程,简略地给出了其规格说明的证明义务,并对其规格说明进行了一次精化。 展开更多

关键词 规格说明 B方法 抽象机 证明义务 精化

下载PDF 职称材料

通过抽象程序证明复杂具体程序 被引量：1

5

作者 李彬 汤震浩 +1 位作者 翟娟 赵建华 《软件学报》 EI CSCD 北大核心 2017年第4期786-803,共18页

描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构(ADTs),如set,list,map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系、抽象程序程序点... 描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构(ADTs),如set,list,map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系、抽象程序程序点和具体程序程序点的对应关系.基于对应关系,抽象程序和具体程序一致性证明可以分解,从而容易并可能自动证明. 展开更多

关键词 程序证明 一致性 抽象程序 精化 分解

下载PDF 职称材料

基于完备抽象解释的性质强保留抽象研究 被引量：1

6

作者 钱俊彦 赵岭忠 蔡国永 《计算机学报》 EI CSCD 北大核心 2014年第8期1754-1767,共14页

在模型检验中,抽象是解决状态空间爆炸问题的重要方法.通常的抽象是非强保留的,即可能存在时序性质在抽象模型不满足而在具体模型满足的情况.文中首先系统地构造μ-演算Lμ语义模型的安全抽象,在此基础上,转换为通用Kripke结构下的安全... 在模型检验中,抽象是解决状态空间爆炸问题的重要方法.通常的抽象是非强保留的,即可能存在时序性质在抽象模型不满足而在具体模型满足的情况.文中首先系统地构造μ-演算Lμ语义模型的安全抽象,在此基础上,转换为通用Kripke结构下的安全抽象.然后基于抽象解释框架及完备抽象解释和性质强保留之间的关系,构造使得Lμ性质强保留的最小抽象模型精化,并转换为抽象解释中抽象域的最小完备精化.依据此完备抽象域求得性质强保留的最优抽象状态划分,从而构造出性质强保留且最优的抽象状态转换系统. 展开更多

关键词 抽象解释 模型检验 性质强保留 完备性 精化

下载PDF 职称材料

一种考虑地图分布信息的分层路径搜索算法 被引量：1

7

作者 李艳 周振华 赵文举 《小型微型计算机系统》 CSCD 北大核心 2013年第11期2607-2611,共5页

目前存在大量的路径搜索算法,但大多数如传统的A*,Dijkstra等算法没有考虑地图中障碍物的分布信息,造成不必要的存储和时间耗费.实际上,搜索空间的分布在很大程度上影响着算法的性能,因此提出一种结合障碍物分布信息和抽象图思想的分层... 目前存在大量的路径搜索算法,但大多数如传统的A*,Dijkstra等算法没有考虑地图中障碍物的分布信息,造成不必要的存储和时间耗费.实际上,搜索空间的分布在很大程度上影响着算法的性能,因此提出一种结合障碍物分布信息和抽象图思想的分层路径搜索算法CDHPA*.该算法首先依据障碍物的分布将地图划分为不均等的子区域,划分区域的数目由可调阈值确定;然后将子区域边界上的非障碍点作为抽象节点来构成完整的抽象图.根据障碍分布,抽象节点之间的最短路径采用曼哈顿距离或自底向上融合算法来计算;最后在抽象图上找到抽象路径并进行细化,得到实际路径.CDHPA*在同一幅地图上进行多次寻路时仅需一次预处理,在线寻路相比同类方法 M-A*、HPA*更快,并且得出的路径为最优路径. 展开更多

关键词 路径搜索 地图分布 抽象图 自底向上 细化路径 最优路径

下载PDF 职称材料

一种基于层次切片的软件错误定位方法 被引量：6

8

作者 许高阳 李必信 +1 位作者 孙小兵 陶传奇 《东南大学学报（自然科学版）》 EI CAS CSCD 北大核心 2010年第4期692-698,共7页

提出了一种基于层次切片模型适合面向对象语言的错误定位方法.首先分别在包层、类层、方法层删去通过测试的包、类和方法,缩小软件错误存在的范围;其次,在语句层将删减后的程序按抽象语法树划分成若干模块,统计模块内变量使用的数目;通... 提出了一种基于层次切片模型适合面向对象语言的错误定位方法.首先分别在包层、类层、方法层删去通过测试的包、类和方法,缩小软件错误存在的范围;其次,在语句层将删减后的程序按抽象语法树划分成若干模块,统计模块内变量使用的数目;通过动态分析,选取一组测试用例计算其执行历史;根据模块内使用变量数目的规模,采用逐步求精算法,计算产生错误测试用例的程序执行历史与静态分析过程中所产生模块的交集及交集的后向切片,直至实现错误定位.实验数据表明:该方法能够查出前期定位程序中绝大部分错误的位置,尤其适用在方法调用比较少的程序中.在方法调用比较频繁的程序中,由于在调用语句处迭代调用逐步求精算法,效率会降低. 展开更多

关键词 层次切片模型 抽象语法树 执行历史 逐步求精

下载PDF 职称材料

基于完备抽象解释的模型检验CTL公式研究 被引量：5

9

作者 钱俊彦 徐宝文 《计算机学报》 EI CSCD 北大核心 2009年第5期992-1001,共10页

在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化... 在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化,并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域,然后通过不动点求解,获得对CTL标准算子完备的最小抽象域,并依据此抽象域求得CTL性质强保留的最优抽象状态划分,最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的. 展开更多

关键词 抽象解释 抽象模型检验 强保留 完备性 精化

下载PDF 职称材料

基于Event-B与ADT的TACS形式化开发方法与验证

10

作者 陈祖希 牛传军 +7 位作者 梅萌 刘杰 刘传振 郑黎晓 骆翔宇 潘亮 汪小勇 徐中伟 《中国铁道科学》 EI CAS CSCD 北大核心 2023年第6期172-183,共12页

为克服Event-B方法在开发全新一代列车自主运行控制系统(Train Autonomous Circumambulate System,TACS)中所出现的建模复杂性问题,提出将抽象数据类型(Abstract Data Types,ADT)实例化与Event-B相结合的方法,对TACS进行形式化开发和验... 为克服Event-B方法在开发全新一代列车自主运行控制系统(Train Autonomous Circumambulate System,TACS)中所出现的建模复杂性问题,提出将抽象数据类型(Abstract Data Types,ADT)实例化与Event-B相结合的方法,对TACS进行形式化开发和验证。首先,根据TACS的需求以及案例研究等相关内容,提取TACS的功能需求和安全需求,并将功能需求和安全需求以非形式化的语言进行描述;然后,根据TACS的功能需求和安全需求进行模型精化层次的设计,避免因在抽象模型中建模复杂的需求而导致证明困难;最后,在模型中使用形式化语言Event-B对TACS的功能需求和安全需求进行建模并验证其正确性,且在建模过程中,利用ADT的抽象概念将轨道网络、轨道区域以及移动授权(Movement Authority,MA)等复杂系统组件在初始模型中指定组件的必要属性,且在后续系统建模过程必要的精化阶段引入组件的具体定义,以降低系统开发和证明的复杂度。结果表明:提出的方法有助于在早期开发阶段减少TACS中复杂的细节部分,使得证明义务成功率为100%,自动证明成功率占比83%,手动证明成功率仅占比仅17%,在简化证明义务的同时有效提高了自动化证明的占比。 展开更多

关键词 EVENT-B 抽象数据类型 精化策略 列车自主运行控制系统

下载PDF 职称材料

General-Service Ballistic Computer Programming Based on B-Method

11

作者 郑宇军 张子丘 +1 位作者 王金全 薛锦云 《Defence Technology（防务技术）》 SCIE EI CAS 2006年第3期178-183,共6页

关键词 抽象机 精化 弹道 程序设计

下载PDF 职称材料