首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到18条相似文献,搜索用时 125 毫秒
1.
随着航天、航空工业的发展,机载嵌入式软件的可信属性验证是新一代飞机研制最关注的软件质量保障问题。形式化方法具有严密的数学基础,能够准确的对系统进行建模、描述和验证,能够在软件系统的设计初期发现潜在的错误,是保证机载软件可信性和安全性的软件正确性验证技术。形式化验证以形式化描述为基础,对所描述系统的特性进行分析和验证,以评判系统是否满足期望的性质,分为定理证明和模型检测两类。文章研究模型检测方法应用于程序形式化描述和验证的技术,提出基于模型检测的验证程序正确性的方案,并进行微内核操作系统程序分析,最后在UPPAAL中进行程序属性的验证。  相似文献   

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

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

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

5.
计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.  相似文献   

6.
《软件》2016,(3):74-78
可信性是各安全攸关领域软件的基础要求,例如航空航天飞行器控制软件、核电站控制软件和交通控制管理软件等,基于形式化方法的程序验证和分析是确保软件正确,具有可信性的重要手段。相比软件测试,基于定理证明的程序验证具有语法和语义的严格性,和属性相关的完备性。本文对程序形式化Hoare语义规约和相关的程序逻辑推理规则系统进行了详细的讨论。基于形式化验证平台Ke Y,采用完全自动化和交互式两种方法,对具有一定规模的,含有循环结构,并且具有实际意义的程序进行验证。研究证明过程的具体证明策略和方法,尤其是关于循环不变式的规约方法;对Ke Y的证明效率,先进性和局限性进行评估。  相似文献   

7.
郭昊  曹钦翔 《软件学报》2022,33(6):2127-2149
霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.  相似文献   

8.
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.  相似文献   

9.
曹钦翔  詹博华  赵永望 《软件学报》2022,33(6):2113-2114
<正>随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.定理证明方法将程序和系统的正确性表达为数学命题,然后使用逻辑推导的方式证明正确性.不同于基于程序测试的技术,定理证明方法能保证覆盖所有边缘情况,完全排除一些特定类型的错误.而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小和复杂性的限制,验证非常复杂的系统和性质.因此,定理证明技术不仅是形式化方法领域,也是众多其他应用领域国内外学者的关注焦点和研究新热点.近年来,定理证明已经逐步用于越来越多的软件、硬件系统验证,这一方面为软硬件系统的安全性保障提供了新的有力工具,另一方面也成为定理证明技术发展的有利契机.目前,定理证明的规模化问题、定理证明工具本身的底层逻辑理论问题、适应于定理证明方案的程序验证理论问题等变得越来越重要,对于数学分析、离散数学、概率等基础定理证明库或求解方案的需求也越来越迫切.  相似文献   

10.
采用数学形式化方法对操作系统进行设计和验证可以保证系统的高度安全性.目前已有的操作系统形式化研究工作主要是验证系统的实现在代码级的程序正确性.提出一种操作系统形式化设计和验证的方法,采用操作系统对象语义模型(OSOSM)对系统的设计进行形式化建模,使用带有时序逻辑的高阶逻辑对操作系统的安全需求进行分析和定义.对象语义模型作为系统设计和形式化验证的联系.以实现和验证过的可信微内核操作系统VTOS为实例,阐述形式化设计和安全需求分析,并使用定理证明器Isabelle/HOL①对系统的设计和安全需求的一致性进行验证,表明VTOS达到预期的安全性.  相似文献   

11.
针对嵌入式机载软件设计中存在的典型缺陷问题,结合嵌入式机载软件任务调度特性,提出采用随机Petri网对嵌入式机载软件设计进行仿真验证的可靠性检测方法,以提高嵌入式机载软件设计的可靠性。该方法采用随机Petri网对嵌入式机载软件系统行为建模,并给出典型缺陷的检测策略和判定准则,然后通过对Petri网模型进行仿真验证,检测系统是否存在此类设计缺陷;并给出了软件设计的运行流程的仿真验证算法,以支持对相应设计的可靠性检测。通过与其他可靠性检测方法的比较,表明了该方法的有效性。  相似文献   

12.
在Hoare逻辑理论和ACSL语法规范的基础上,设计一种针对密码软件的形式化验证系统,由程序规范、验证推理规则、可靠性策略、验证推理等模块组成。以OpenSSL中RC4算法的软件实现为例,对其功能正确性、保险性和信息流安全性进行验证,结果表明,该系统具有较高的自动化水平,可在一定程度上降低形式化验证方法的复杂度。  相似文献   

13.
Auxiliary variables are essential for specifying programs in Hoare Logic. They are required to relate the value of variables in different states. However, the axioms and rules of Hoare Logic turn a blind eye to the role of auxiliary variables. We stipulate a new structural rule for adjusting auxiliary variables when strengthening preconditions and weakening postconditions. Courtesy of this new rule, Hoare Logic is adaptation complete, which benefits software re-use. This property is responsible for a number of improvements. Relative completeness follows uniformly from the Most General Formula property. Moreover, one can show that Hoare Logic subsumes Vienna Development Method's (VDM) operation decomposition rules in that every derivation in VDM can be naturally embedded in Hoare Logic. Furthermore, the new treatment leads to a significant simplification in the presentation for verification calculi dealing with more interesting features such as recursion. Received October 1998 / Accepted in revised form October 1999  相似文献   

14.
The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect to the operational semantics of CompCert Clight. This paper introduces VST-Floyd, a verification assistant which offers a set of semiautomatic tactics helping users build functional correctness proofs for C programs using Verifiable C.  相似文献   

15.
一种用于指针程序安全性证明的指针逻辑   总被引:7,自引:3,他引:4  
在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析,所获得的信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质.  相似文献   

16.
面向适航标准的机载软件测试验证工具综述   总被引:1,自引:0,他引:1       下载免费PDF全文
机载软件的测试与验证是保障机载软件正确性和可靠性的重要方法。软件的测试与验证离不开工具的支持,使用工具能够提高效率、降低成本,对机载软件的测试验证工具研究是对其进行充分测试验证的保障。对机载软件及适航标准进行了简介;按照系列适航标准,从DO-178C、基于模型的开发与验证(DO-331)和形式化方法(DO-333)三个维度对工具的功能、特性及应用进行了详细介绍,并对其发展现状进行小结;总结机载嵌入式软件测试验证及其工具研发中存在的问题,并对其发展趋势进行了分析。  相似文献   

17.
Proving pointer programs in higher-order logic   总被引:2,自引:0,他引:2  
Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higher-level data types for verification. The programming language is embedded in higher-order logic. Its Hoare logic is derived. The whole development is purely definitional and thus sound. Apart from some smaller examples, the viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr–Waite graph marking algorithm and present part of its readable proof in Isabelle/HOL.  相似文献   

18.
机载软件测试是指机载系统中嵌入式软件执行的测试验证过程,目的是为了挖掘出软件缺陷从而提高机载系统的可靠性。随着机载嵌入式系统功能的多样化需求,软件的规模和复杂程度不断增加,同时因为其实时性、嵌入性、高可靠性等特殊性,因此对机载软件进行充分测试成为当前的一个挑战。为了满足要求,机载系统的测试需要遵循最新的适航标准DO-178C,针对机载软件生命周期过程提出了一系列目标要求和设计考虑。为此,简介了机载软件适航认证标准的发展及其测试环境;根据DO-178C对机载软件测试的各个过程从基于需求、基于模型、基于安全性分析以及软件验证的测试研究机载软件的测试验证方法,并进行小结;对相关领域的发展进行总结和展望。  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号