基于分离逻辑的程序验证技术 被引量：7

1

作者 黄达明 曾庆凯 《软件学报》 EI CSCD 北大核心 2009年第8期2051-2061,共11页

介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入... 介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向. 展开更多

关键词 可信软件 程序验证 霍尔逻辑 分离逻辑 定理证明

下载PDF 职称材料

基于分离逻辑的云存储系统验证 被引量：4

2

作者 金钊 王捍贫 +2 位作者 张博闻 张磊 曹永知 《计算机学报》 EI CSCD 北大核心 2020年第12期2227-2240,共14页

数据的快速增长限制了传统存储技术存储和管理数据的能力,云存储系统应运而生.云存储系统最重要的特征是数据以块的形式存储,且每个块被视为一个独立的存储单元.因此,云存储系统通常包含两种存储单元:原始地址和块地址,这使得云存储系... 数据的快速增长限制了传统存储技术存储和管理数据的能力,云存储系统应运而生.云存储系统最重要的特征是数据以块的形式存储,且每个块被视为一个独立的存储单元.因此,云存储系统通常包含两种存储单元:原始地址和块地址,这使得云存储系统与传统内存系统相比有着显著的不同.从而,如何保证云存储系统的可靠性成为了有待解决的难题.本文基于分离逻辑提出了一种系统方法来验证云存储系统管理程序的正确性.主要贡献包括:(1)提出了一种建模语言来描述云存储管理;(2)扩展了分离逻辑的断言语言来描述云存储系统中有关块的属性;(3)在上述两个语言的基础上,提出了一套霍尔型的规范规则对云存储系统进行推理.规范的前置和后置条件都以断言对的形式给出.运用这些方法,能够验证云存储管理程序的正确性. 展开更多

关键词 分离逻辑 霍尔逻辑 云存储系统 建模语言 形式验证

下载PDF 职称材料

采用数据通道工作方式的商用计算机管理软件 被引量：3

3

作者 刘斌 《电子技术应用》 1981年第1期18-20,24,共4页

随着计算机应用技术的推广,电子计算机不仅可以用来进行各种类型的科学计算和数据处理,而且逐渐地在商业上将会得到极其广泛的应用。本文着重介绍商业应用电子计算机管理网络中的《商用键盘终端的计算机管理》部分。即商用键盘终端在DJS... 随着计算机应用技术的推广,电子计算机不仅可以用来进行各种类型的科学计算和数据处理,而且逐渐地在商业上将会得到极其广泛的应用。本文着重介绍商业应用电子计算机管理网络中的《商用键盘终端的计算机管理》部分。即商用键盘终端在DJS-130计算机采用数据通道工作方式的软件。《商用键盘终端的计算机管理》是商业零售环节计算机管理的一个重要部分。其技术方案是:由一台DJS-130电子计算机和一台与电子计算机快速交换数据和信息的《商业专用接口》及若干台键盘终端设备组成。若干台键盘终端均放置在商店的营业柜台上。 展开更多

关键词 地址变量 计算机 输入输出通道 数据通道 霍尔逻辑 数理逻辑 程序逻辑 清零 计算机系统 程序系统 终端显示 键盘 计算机辅助管理 计算机管理 数据处理 符号处理

下载PDF 职称材料

复杂内核数据结构程序形式化验证

4

作者 李薛剑 余韵 《计算机系统应用》 2023年第11期253-266,共14页

操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节,但是,在实际的验证工作中,操作系统内核中全局性质的不变式定义,复杂数据结构程序的形式化描述和验证仍存在很多困难.本文针对操作系统内核中满足的全局... 操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节,但是,在实际的验证工作中,操作系统内核中全局性质的不变式定义,复杂数据结构程序的形式化描述和验证仍存在很多困难.本文针对操作系统内核中满足的全局性质,在代码层以函数为单位,用全局不变式进行定义,并在不同的函数中进行形式化验证,从而证明各个函数符合操作系统内核的全局性质;针对操作系统内核中经常使用的复杂数据结构程序,本文通过扩展形状图理论,提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序,并对该方法进行了正确性证明,最终成功验证操作系统内核中关于任务创建与调度,消息队列创建与操作相关的代码. 展开更多

关键词 形式化验证 内核验证 内核数据结构 霍尔逻辑

下载PDF 职称材料

基于隔离逻辑的并行程序可靠性验证方法 被引量：2

5

作者 万良 《计算机工程》 CAS CSCD 2014年第2期86-91,96,共7页

并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大,使得验证的内容和目标之间的关系不明确。为解决该问题,提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图,描述变量相关的语句及执行关系,... 并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大,使得验证的内容和目标之间的关系不明确。为解决该问题,提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图,描述变量相关的语句及执行关系,将所需验证的程序性质逻辑式转换为变量并行语句序列的逻辑组合式,使得性质表达式与并发程序的语句相关联。根据逻辑组合式确定语句执行序列和前后件逻辑表达式,基于并发隔离逻辑的公理系统对语句执行序列进行验证,并根据验证结果对并发程序进行修改和完善。通过对银行柜台业务办理的功能模块验证结果表明该方法是有效的。 展开更多

关键词 霍尔逻辑 隔离逻辑 并行程序 逻辑组合式 可靠性验证

下载PDF 职称材料

一种用于类C语言环境的安全的类型化内存模型 被引量：3

6

作者 何炎祥 吴伟 +2 位作者 陈勇 李清安 刘健博 《计算机研究与发展》 EI CSCD 北大核心 2012年第11期2440-2449,共10页

使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无... 使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无法保证安全性,同时使程序验证变得异常复杂.面向对象语言的内存模型则具有较高的抽象性,便于程序验证,但不适合描述低级的内存操作.结合字节内存模型和面向对象语言内存模型,提出一种安全的类型化的内存模型,既可用于对语义的形式化,也可用于基于霍尔逻辑的程序验证.此内存模型既允许指针算术、结构赋值、类型转换等内存操作,同时也可以有效减少因指针别名给程序验证带来的复杂度.基于Coq辅助定理证明工具,对内存模型进行了形式化实现和验证. 展开更多

关键词 操作语义 形式化验证 内存模型 霍尔逻辑 内存安全

下载PDF 职称材料

基于Coq的微内核操作系统程序验证方法研究 被引量：3

7

作者 张忠秋 董云卫 +1 位作者 张雨 张凡 《计算机测量与控制》 CSCD 北大核心 2011年第8期1939-1942,共4页

机载嵌入式程序的可信属性验证是新一代飞机研制最关注的软件质量保障问题;基于定理证明的程序形式化验证方法是一种可靠和严格的软件正确性验证技术;文中在深入分析微内核操作系统的基础上,应用霍尔逻辑针对机载嵌入式软件核心代码开... 机载嵌入式程序的可信属性验证是新一代飞机研制最关注的软件质量保障问题;基于定理证明的程序形式化验证方法是一种可靠和严格的软件正确性验证技术;文中在深入分析微内核操作系统的基础上,应用霍尔逻辑针对机载嵌入式软件核心代码开展程序验证技术研究,根据霍尔逻辑的相关推理规则进行程序验证,并在定理证明辅助工具Coq中形式化表示霍尔逻辑的推理规则,针对机载操作系统的部分程序代码实例进行验证;实验结果表明基于定理证明的程序验证方法可以对软件程序代码的正确性进行验证,从而帮助软件提供商开发高可信的机载嵌入式软件。 展开更多

关键词 程序验证 霍尔逻辑 推理系统 定理证明

下载PDF 职称材料

基于分离逻辑的并行程序性质验证方法

8

作者 万良 石文昌 冯慧 《计算机科学》 CSCD 北大核心 2013年第10期148-154,共7页

随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出。并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大。为此,提出一种基于分离逻辑的新的验证方... 随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出。并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大。为此,提出一种基于分离逻辑的新的验证方法。该方法根据分离逻辑的程序语义描述兼有解释语义和公理语义的特点,从验证的性质出发,把要验证的性质式转换成并行语句序列的逻辑组合式,并进行整理和化简;然后,利用分离逻辑公理系统对语句序列进行验证,用验证了的断言集来求出性质的真值。实例进一步说明,此方法更有效,同时也简化了验证的规模。 展开更多

关键词 霍尔逻辑 分离逻辑 并行程序 逻辑组合式 性质验证

下载PDF 职称材料

基于Hoare逻辑的密码软件安全性形式化验证方法

9

作者 肖堃 《吉林大学学报（工学版）》 EI CAS CSCD 北大核心 2019年第4期1301-1306,共6页

为了解决密码软件安全性验证效率和准确率低的问题,提出了基于Hoare逻辑的密码软件安全性形式化验证方法。首先对密码软件的主要性质进行描述,然后通过密码软件运行时随机向量的分析,得到密码软件运行的矩阵表达式,再将其进行线性变换,... 为了解决密码软件安全性验证效率和准确率低的问题,提出了基于Hoare逻辑的密码软件安全性形式化验证方法。首先对密码软件的主要性质进行描述,然后通过密码软件运行时随机向量的分析,得到密码软件运行的矩阵表达式,再将其进行线性变换,计算密码软件运行时数据的方差和协方差矩阵,获得密码软件运行时数据矩阵的主成分空间,并对密码软件运行的主成分进行分析;最后,利用密码软件的逻辑模型和软件运行的状态集合对密码软件安全形式化验证的流程进行分析,建立密码软件的运行模型并设置安全属性,并将密码软件运行时出现的故障进行标记和处理,得到密码软件运行的安全结果,从而实现密码软件安全性形式化的验证。实验结果表明,采用该方法对密码软件的安全性进行验证具有较高的效率,且能够准确地验证密码软件的安全。 展开更多

关键词 计算机系统结构 霍尔逻辑 密码软件 安全性验证

原文传递

基于Isabelle/HOL的安全操作系统形式化验证方法

10

作者 郭毅 杨维永 刘苇 《计算机与现代化》 2017年第4期99-104,共6页

操作系统作为信息时代的基石,其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法。本文提出一种软件形式化验证的新思路:通过在Isabelle中构造模拟运行环境,使汇编代码运... 操作系统作为信息时代的基石,其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法。本文提出一种软件形式化验证的新思路:通过在Isabelle中构造模拟运行环境,使汇编代码运行其中,并记录系统状态的变化,最终根据程序运行前后系统状态的变化情况判断程序的正确性和安全性。重点介绍了顺序、分支和循环等3种程序结构的证明方法,并通过一个程序实例证明,得到在任意前提条件下程序执行前后系统状态的变化情况。 展开更多

关键词 安全操作系统 形式化验证 Isabelle/HOL 霍尔逻辑

下载PDF 职称材料

基于交互式定理证明的并发程序验证工作综述

11

作者 王中烨 吴姝姝 曹钦翔 《软件学报》 EI CSCD 北大核心 2024年第9期4069-4099,共31页

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用.但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果.同时,并发程序执行时的不确定... 并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用.但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果.同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难.在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证.对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性.交互式定理证明方法中常用程序逻辑对程序进行验证,分析基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用这些方法的程序验证工具和程序验证成果进行总结. 展开更多

关键词 并发程序验证 可线性化 上下文精化 程序逻辑 关系霍尔逻辑

下载PDF 职称材料

机载雷达伺服驱动异常分析与场景重现 被引量：1

12

作者 柳尚光 钟永磊 《电子质量》 2020年第9期36-38,共3页

机载雷达伺服分系统具有良好的快速跟踪性能,以PWM加功率模块构成的功放电路作为功率驱动部分。该例中,功放驱动电路中的4只驱动器无输出,内部MOS管不同程度损伤。电路输出异常,电机不工作。通过分析驱动电路工作原理,检查电流闭环控制... 机载雷达伺服分系统具有良好的快速跟踪性能,以PWM加功率模块构成的功放电路作为功率驱动部分。该例中,功放驱动电路中的4只驱动器无输出,内部MOS管不同程度损伤。电路输出异常,电机不工作。通过分析驱动电路工作原理,检查电流闭环控制电路、欠压保护电路、电路损伤情况等,开展模拟试验复现样品内部MOS管损伤形貌,最终判断产品外围控制电源异常导致产品电流环失控,产品输出过流,使得局部热积累并导致MOS管热击穿。 展开更多

关键词 雷达 功率驱动 脉宽调制 霍尔换向逻辑

下载PDF 职称材料