断言语言支持自定义谓词的程序验证器原型

基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质.     

基于抽象内存模型的内存相关漏洞检测方法

针对现有的内存相关漏洞检测方法中存在依赖指针数据流而导致大量误报漏报、缺乏漏洞特征的形式化描述以及漏洞特征描述不全面的问题,提出一种基于抽象内存模型的内存相关漏洞检测方法.对抽象内存模型进行相关定义;基于抽象内存模型,对内存泄露、重复释放内存和读写释放后的内存这三种与内存相关的漏洞类型的特征进行形式化符号表示;基于代码...     

基于Event-B的航天器内存管理系统形式化验证

内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会较之前的验证工作带来更多难题,主要体现在：内存管理模块中的复杂数据结构的形式化描述;操作的规范语义;行为的建模;内部函数的规范及断言定义与循环不变式的定义;实时性验证等方面.本文拟针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法,来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.本文研究成果有望被直接应用于我国新一代的航天器系统上.     

基于函数式语义的循环和递归程序结构通用证明技术

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

基于抽象解释的Prolog程序验证技术研究

作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中.现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键.本文给出了一种基于抽象解释的Prolog程序验证方法,该方法采用了具有路径信息的Prolog语义及其抽象作为语义基础,因而可用于验证与程序点相关联的程序特性.本文例子表明了该验证方法的有效性.     

一种从Z到精化演算的软件开发方法

一、引言形式化方法的研究和应用已有二十多年的历史,源于Dijkstra和Hoare的程序验证以及Scott、stratchey等人的程序语义研究,指为保证复杂系统的可靠性,以数学为基础对其进行精确描述和验证的语言、技术和工具。形式化方法的关键在于形式规约语言。通过语法和语义有严格数学定义的形式规约语言对系统及其各方面性能的描述,产生系统的形式规约,可以帮助开发者获得对所描述系统的深刻理解,并通     

面向顺序存储结构的数据流分析

C程序中数组、malloc动态分配后的连续内存等顺序存储结构被大量使用，但大多数传统的数据流分析方法未能充分描述其结构及其上的操作，特别是在利用指针访问顺序存储结构时，传统的分析方法只关注了指针的指向关系，而未讨论指针可能发生偏移的数值信息，且未考虑发生偏移时可能存在越界的不安全问题，导致了对顺序存储结构分析不精确.针对以上不足，首先对顺序存储结构进行抽象建模，并对顺序存储结构与指针结合使用时的指向关系与偏移量进行有效表示，建立了用于顺序存储结构的抽象内存模型SeqMM；其次，归纳总结C程序中顺序存储结构涉及的指针相关迁移操作、谓词操作及遍历顺序存储结构的循环操作，提出了安全范围判别保证操作安全性；之后，针对函数调用时形参指针引用顺序存储结构与实参的映射过程进行过程间推导规则设计；最后，基于上述分析，提出了一种内存泄漏缺陷检测算法对5个开源C工程的内存泄漏缺陷进行检测.实验结果表明：所提出的SeqMM能够有效地刻画C程序中的顺序存储结构及其涉及的各种操作，其数据流分析结果能够用于内存泄漏的检测工作，同时在效率和精度之间取得合理的权衡.     

基于Object-Z的XPath形式化语义

本文描述了XPath语言的形式化语义。一个统一的面向对象的语义视角用于建模所有XPath语言构造。语义的表示采用形式化规范语言Object-Z的符号系统。这种高度结构化的语义模型具有简洁、可组合性和可复用性的特点。     

单元自动化测试中类的抽象内存模型研究

由于面向对象程序具有多态性等复杂特性,在软件单元测试中仅凭静态分析难以判断指针和引用指向对象的具体类型,为了解决这一问题,对类的抽象内存模型进行研究,并提出类的操作语义模拟算法;在路径分析时,通过构建和更新抽象内存模型,从而对变量所属类的范围进行限定;对于单元测试,对基于输入域的随机测试进行优化,提出基于路径的随机测试方法,得到输入变量的类型集合;实验表明,类的抽象内存模型结合操作语义模拟算法能够有效提取出路径中类相关的约束,基于路径的随机测试方法比起基于输入域的随机测试方法能够明显提高测试效率。     

基于时序逻辑的UML2.0通信图语义研究

UML2.0通信图可以表示对象之间的交互,很适合用于对系统的交互行为建模,但由于UML缺乏精确语义,使得难以对其所表示的系统行为进行分析和验证.XYZ/E是可执行线性时序逻辑语言,既可描述系统的静态语义和动态语义.在定K.UML2.0通信图的形式化语法的基础上,给出了通信图的XYZ/E时序逻辑语义,为进一步的系统分析和验证提供了形式化基础.