形式化验证

摘要： 根据联锁系统的形式化验证系统需求,设计一种联锁数据翻译器软件的总体方案,实现站点接口文件、T LE文件和布尔逻辑文件等文件的翻译转换,生成形式化验证所需要的LCF文件。最后详细说明翻译器软件基于函数式语言OCaml的代码实现。

摘要： 区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用定理证明的形式化方法,基于交互定理证明器HOL-Light中集合库、实分析库等定理证明库,实现了群机器人工作场景的高阶逻辑表达;完成了机器人移动概率和平均移动概率的建模与验证;最终验证了一定时间步长内群机器人在特定区域内的覆盖率的正确性.为实现多种复杂场景下群机器人区域覆盖算法的高阶逻辑定理证明形式化分析奠定基础.

摘要： 针对代币智能合约的形式化验证方法中模型检测存在的状态空间爆炸问题,提出了一种两段式模型检测方法。使用图转换规则对智能合约建模,利用工具生成模型状态空间。第一阶段对部分状态空间进行分支时序逻辑验证后,第二阶段先使用前一阶段的状态验证信息构造马尔可夫链,使用集束搜索结合马尔可夫链对余下状态进一步筛选,再进行验证。实验结果表明,该方法能够有效减少需验证状态数量,解决状态空间问题,完成合约验证。

摘要： 以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点。定理证明需要强大的形式化规约表达能力作为基础。文章对现有以太坊智能合约的定理证明研究中使用的形式化规约表达方法进行综述,从智能合约开发语言和区块链内生语义的建模、智能合约安全属性和功能属性的形式化规约表达、自动定理证明和交互式定理证明的选择等角度对形式化规约方法进行比较和讨论,并指出目前的困难和未来的研究方向。

摘要： 云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.

摘要： 飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.

摘要： 由于系统资源的有限性,目前空间飞行器中的嵌入式操作系统并没有文件系统模块.系统任务通过直接调用I/O接口,完成外部存储设备的读与写.但是,随着空间飞行任务复杂化,数据大量涌现,空间嵌入式操作系统需要文件系统来完成数据处理,因此安全可靠的文件系统的开发是空间嵌入式操作系统亟待解决的问题.空间嵌入式操作系统是典型的安全关键的系统,集成在系统中的每一个模块都需要经过严格的测试,保证其不会在运行期间产生故障.采用形式化验证的技术可以从数学上严格保证验证对象的正确性.因此,本文采用形式化技术,针对面向空间飞行器文件系统的需求,验证其内部逻辑的正确性.

摘要： 安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的3层开发框架相结合,通过性质分层传递验证的方法,保证了各个层次间的一致性.首先,从需求层面的需求分析开始,引入形式化证明的思路,证明对需求层逻辑的正确性,从而可以更好地指导程序的设计.其次,在设计层面的验证可以极大地减少开发代码的错误率,证明设计算法和需要实现的函数之间调用逻辑的正确性.最后,在实现层,证明所实现代码与函数设计的一致性,并且证明代码实现的正确性.使用交互式定理证明辅助工具Coq,以某一国产空间嵌入式操作系统的内存管理模块为例,证明了其内存管理算法的正确性以及需求、设计、实现的一致性.

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

摘要： 可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.

摘要： 随着集成电路设计技术的发展与复杂算法设计的需求的增加,大规模集成电路设计中规模将会呈现爆炸性的增长,不可避免会遇到验证不充分的问题.针对需求规格难以验证完备的问题,提出了基于属性描述语言的形式化验证方法,利用属性描述语言将设计中的可见需求和隐含需求以断言的形式增加到形式验证中,给出典型功能模块的断言表示并通过JasperGold工具进行实验.

摘要： 随着半导体工艺的进步,片上存储器的设计容量和复杂度日益增加,传统的功能验证方法面临着验证正确性、效率、完备性等方面挑战.采用基于System Verilog Assertions的方法对全局Cache进行形式化验证.利用形式化验证工具Incisive Formal Verifier自动产生符合约束的激励后,对测试表达式进行实时监控、检测,并在断言违反处报错、给出反例波形.通过形式化验证和传统验证的对比实验,得到在模块级层次上形式化验证的模拟效率总体高于传统验证的结论.

摘要： 铁路联锁系统设计通常采用梯形逻辑进行建模.为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证.

摘要： 随着软件系统的结构越来越复杂，规模越来越庞大，复杂程度越来越高，软件出现错误的可能性及其造成的危害也日益突出，由于软件错误而导致灾难性后果的报道屡见不鲜。在这些错误中有一些是致命的错误，如果不及时发现就会导致生命与财产的重大损失。这种情况迫使人们必须投入大量的精力对软件进行测试。本文研究了软件形式化方法,提出了基于形式化验证的软件失效模型描述形式化表示方法,将形式化方法应用于程序语法描述,对程序的语义进行准确的定义,并完成了对内存管理失效模型和控制流失效模型的形式化描述.进一步研究了语义规约的过程中自动识别和定位前文所述的常见失效模型的匹配定位算法,并通过工具实现了上述两个失效模型的软件缺陷自动化检测。

摘要： 近年来,随着对于安全关键类软件系统研发的要求不断提高,形式化方法被越来越多的应用于软件系统研发过程中.使用形式化方法依赖形式化语言及其对应的形式验证工具,Why3语言作为形式化语言的一种,因其特性比较符合安全关键类软件系统的形式化验证,正在越来越多的被使用.由于当前Why3缺乏相关整合的形式验证工具,使Why3语言的使用难度增加,所以需要实现一种基于Why3的形式验证工具.本文主要阐述了基于形式化语言Why3的形式验证工具的实现,并使用实现的工具对于ARINC 653标准中的一个案例进行验证.文章首先进行了形式化方法及语言的相关介绍,然后阐述了基于Why3的形式验证工具的实现,最后描述了使用实现的工具对ARINC 653标准中的一个案例进行验证的过程.

摘要： 形式化软件方法采用数学的方法对软件进行建模和验证,可提高软件安全性.本章讨论了软件的形式化开发方法,讨论了形式化验证的问题,重点关注了论了定理证明和模型检验的局限性,综述了当前降低模型检验开销的研究进展.

摘要： 如今的CPU结构十分复杂,传统的测试、模拟等验证方法无法完全保证CPU结构设计的正确性.针对CPU结构设计的正确性验证问题,本文基于CPU结构模型建立了CPU结构公理系统,提出了在此公理系统上进行定理证明的形式化方法,开发了自动验证工具,并对MIPS指令集上的CPU结构设计进行了验证.

摘要： 工业控制计算机是一种采用总线结构,对生产过程及其机电设备、工艺装备进行检测与控制的设备的总称.随着技术的快速发展,目前工业控制计算机的概念已超越了这种传统定义,正在涉及计算机科学中越来越多的技术和领域,向着标准化、网络化、智能化、并行处理和高可靠的方向发展.本文针对工业控制计算机快速发展的现状,紧紧围绕工业控制计算机的发展历程及其关键技术,主要论述了三方面的内容.首先,重点论述了总线技术革新驱动下工业控制计算机的发展历史和现状,并对工业控制计算机发展趋势和前景进行了展望.其次,介绍了当前工业控制领域最重要的嵌入式系统中涌现的新技术,即片上系统、片上网络、片上多核并行处理及多核操作系统等.最后,针对工业控制中高可靠和高安全的特殊领域,介绍了当前广泛应用的容错计算机体系结构、可重构技术以及软件形式化验证技术.

摘要： 状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的程序建模语言.事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用.文中针对这些问题,首先提出层次化时间状态迁移矩阵(Hierarchical Time State Transition Matrix, HTSTM)模型,用于设计、建模和验证具有时间条件约束的软件系统,并给出形式化表示方法.基于该表示方法提出一种符号化编码方法,采用有界模型检测思想将需要验证的LTL性质输入SMT(Satisfiability Modulo Theories)求解器进行验证,从而在一定程度上证明了软件设计的正确性.

摘要： 浮点部件是微处理器的核心部件之一,其正确性验证非常重要,然而由于逻辑的复杂性,浮点部件的验证是处理器正确性验证的一大挑战.本文设计了基于双参考模型的模拟验证和基于算法模型和工具的形式验证两种方法,其中模拟验证中,利用SoftFloat和x86浮点运算作为混合双参考模型,提高了参考模型的正确性,同时还设计了浮点加扰激励,以增强对边角情形的测试力度;形式验证用于验证浮点加减、比较和转换运算的正确性.两种方法的结合能够提高验证效率,同时能更好地保证验证的完整性.根据本文提出的方法,在某浮点部件的验证中,发现逻辑错误5个,并发现了与x86处理器浮点运算的一些细微差别,确保了芯片的成功流片.

摘要： 本文描述的一个实施例涉及一种用于监督动态系统(例如交通工具)的方法。该方法包括接收系统状态样本，以及针对特定时刻、基于当前系统状态和表示动态系统的系统模型来计算系统状态的可达集合。该方法还包括计算通用规则的特定表现形式的数学表示，并且基于可达集合和通用规则的特定表现形式的数学表示来计算系统状态的允许子集。此外，该方法包括测试系统状态样本是否在允许子集内。

摘要： 本发明公开了一种应用于针对源代码的运行时形式化验证方法中的验证系统，所述系统包括：切面类文件及监视器文件自动生成工具，用户可定义描述程序性质的LTL线性时态逻辑公式以及配置文件，通过该工具自动生成监测程序性质的切面类以及监测程序状态的检测器；通过将修改后的SystemC的仿真内核与运用切面类形式的插桩源代码，以及检测器联合编译，形成可运行目标文件，运行该文件，以检测程序的动态执行，实时验证系统的性质。本发明可以应用到嵌入式系统及大型软件系统的形式化验证中，能够提高软件的安全性、可靠性。

摘要： 本发明公开了一种基于形式化验证的芯片IO复用验证方法，包括如下步骤：S1、根据芯片规定定义，提炼芯片IO复用关系文件；S2、根据芯片IO复用关系文件，自动形成IO描述文件；S3、开启形式验证，同时导入芯片文件和IO描述文件到验证工具；S4、启动形式化验证，输出验证结果；S5、分析结果，判断是否为设计BUG。优点，本发明验证方法，相比传统的Uvm验证,基于形式化验证的IO复用验证技术使用简单，步骤简洁，大幅降低了工作量；该方法无需芯片系统级仿真运行，因而运行时间短，大幅提升了验证效率。

摘要： 本申请提供一种基于形式化验证快速收敛覆盖率的验证方法及装置，DUT为amba总线的协议转换模块，如AHB2APB模块、AXI2AHB模块或AXI2APB模块等。针对能够覆盖的DUT行为，利用形式化仿真器穷举输入信号的行为并生成测试激励，基于统一覆盖率的验证结果分析，如果验证结果达不到要求，将结果反馈给验证计划，使得验证平台更容易建立、覆盖率更容易收敛，通过形式化验证避免了在验证至覆盖率较高后的验证效率降低，缩短了覆盖率收敛时间，提高了验证效率。

摘要： 本申请提供了一种基于形式化验证的智能合约功能验证方法及装置，所述方法包括以下步骤：获取待验证的智能合约数据，对所述智能合约数据进行编译，判断编译是否通过，若编译通过，将所述智能合约数据转化为中间语言，根据所述中间语言，通过规则库生成测试用例，根据所述测试用例验证智能合约数据，得到验证结果。本申请通过依据solidity的行为将其抽象为模型可识别的中间验证语言，方便模型生成测试用例。根据测试用例对智能合约内的功能进行快速验证，解决了现有智能合约验证方法审计时间长、审计效率低的问题。

摘要： 本发明提供了一种基于形式化验证的软件开发模型的验证方法，将形式化验证与软件开发过程结合起来，提高软件的高可信程度，从逻辑上保障开发软件的可靠性；发挥形式化验证在软件检错领域的对于软件开发过程中开发逻辑进行验证的作用；降低程序在非正常状态运行的可能性。本发明提高软件的高可信程度，从逻辑上保障开发软件的可靠性；在需求阶段进行验证，可以避免因为软件需求分析不合理导致重新开发的严重后果；及时发挥形式化验证在软件检错领域的对于软件开发过程中函数逻辑正确性进行验证的作用；将形式化方法引入软件开发过程，并给出具体的模型，解决了测试技术在软件检错领域的局限性问题。

摘要： 本发明公开了一种用于联锁软件形式化验证的系统模型构建方法，涉及计算机联锁系统技术领域。本发明利用采用不同的编程方法和编程语言开发的两个具有相同功能的翻译器读取联锁输入数据；并通过文件比较工具对两个具有相同功能的翻译器输出的特点格式的数据文件进行一致性校验；采用编程方法开发一个系统模型构建工具，利用该系统模型构建工具读入S1步骤中经翻译器数据转换后且通过一致性校验的特定格式文件，依据特定格式文件构建系统模型。本发明从信号人员视角出发，重点描述联锁数据层面的系统模型构建，及其与对象模型的映射关系。本发明描述的系统模型构建方法为信号人员如何依据现有联锁数据构建系统模型提供了一种思路。

摘要： 本发明公开了一种基于形式化验证的嵌入式设备安全启动方案设计方法，基于形式化的分析与验证，通过分析威胁模型，得到安全需求，并以此为基础建立形式化模型，最终转换成安全启动方案，并通过定理证明的方法确保嵌入式设备安全启动方案的可用性和安全性，本发明针对嵌入式系统设备在安全启动过程中存在的安全性问题，提供了一种基于形式化验证的解决方法。该方法系统全面地分析了安全启动过程中所面临的问题，给出具体的安全启动方案设计，并通过使用定理证明的方法给出具体方案的可用性和安全性的证明，本发明不仅可以快速的解决安全启动过程中的威胁，还从理论上证明了方案的安全性和可靠性。

摘要： 本发明公开了一种基于属性自动提取和形式化验证的硬件木马搜索检测方法，包括以下步骤：输入待检测集成电路设计；将集成电路设计综合成FPGA网表；对FPGA网表进行随机功能仿真，并保存信号行为列表；结合FPGA网表对信号行为列表进行分析，得到收敛至稳定集合下的低翻转率信号列表与低覆盖率LUT列表；根据低翻转率信号列表与低覆盖率LUT列表，提取集成电路设计的定常属性；对所提取的属性进行形式化验证，搜索待检测集成电路设计中隐含的硬件木马的触发条件，从而实现木马检测。本发明方法能够搜索到基于特定条件激活以及基于集成电路内部可满足性无关项的硬件木马触发条件，可在集成电路设计早期实现木马的检测和定位。

摘要： 本发明公开了一种形式化验证方法、系统、装置及计算机可读存储介质，属于电力能源领域，包括如下步骤：根据应用场景的用能需求，确定能源综合服务站的功能定位、组合元素，构建能源综合服务站的供能模型；建立能源综合服务站运行管控模型，通过分析上传的运行数据以及控制能源站内部各设备的运行状态，使能源综合服务站满足实时的功率平衡需求；通过所述供能模型、能源综合服务站运行管控模型，对规划的能源综合服务站信息物理系统使用形式化方法验证，计算其运行时非正常状态的次数、发生时刻以及持续时间，从而修正能源综合服务站与监控系统规划时出现的错误。解决了现有能源综合服务站规划方案存在局限性、可靠性差的技术问题。