摘要：通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用 ,同时对布尔函数在计算机内的表示二叉判定图 (BDD)进行了进一步地分析 。

摘要：为确保拟态路由器中协议代理等“拟态括号”关键组件的安全性和功能正确性,设计实现了边界网关协议(BGP)代理,并采用形式化方法对BGP代理的安全性和功能正确性进行了验证。BGP代理通过监听邻居路由器与主执行体之间的BGP会话报文,模拟邻居路由器与从执行体展开BGP会话,实现各执行体的BGP状态一致。采用VeriFast定理证明器,编写基于分离逻辑的形式化规约,证明程序不会出现空指针引用等内存安全问题,并验证了BGP代理各功能模块实现的高级属性符合功能规约。BGP代理实现与验证代码量之比约为1.8:1,程序设计实现和程序验证所耗费的时间之比约为1:3。经过形式化验证的BGP代理处理100000条BGP路由所花费的时间为0.16 s,约为未经过验证的BGP代理的7倍。研究工作为应用形式化方法证明拟态防御设备与系统中关键组件的安全性和功能正确性提供了参考。

摘要：为提高下一代列车运行控制(简称列控)系统安全计算机的系统兼容性,首先对其结构进行简要分析,并对管理机制进行设计,建立了管理单元状态转移模型,同时以形式化验证工具对模型的正确性进行了验证。在此基础上对基于微控制单元(MCU,micro controller unit)的管理单元进行了软硬件的设计实现与测试。验证和测试结果表明,所设计的管理机制符合设计规范的要求,管理单元能够实现预期的状态转移功能。

摘要：DH坐标系在机器人运动学分析中发挥着重要的作用.在基于DH坐标系构建的机器人控制系统中,机器人结构的复杂性使得构建安全的控制系统成为一个难题,仅依靠人工方法可能导致系统漏洞和安全风险,从而危及机器人的安全.形式化方法通过演绎推理与代码抽取实现了对软硬件系统的设计、开发及验证.基于此,设计基于DH标定的机器人正向运动学的形式化验证框架.在Coq中构建机器人运动理论的形式化证明,并验证控制算法的正确性以确保机器人的运动安全.首先,对DH坐标系进行形式化建模,构建相邻坐标系间转换矩阵的形式化定义,并验证该转换矩阵与复合螺旋运动的等价性;其次,构建机械臂正向运动学的形式化定义,并对机械臂运动的可分解性进行形式化验证;再次,对工业机器人中常见连杆结构及机器人进行形式化建模,并完成正向运动学的形式化验证;最后,实现Coq到OCaml的代码抽取,并对抽取的代码进行分析与验证.

摘要：分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格证明设计模型中目标性质的正确性,适合用于验证共识协议.然而,随着分布式系统的规模增大,问题复杂度提升,使得分布式共识协议的形式化验证更为困难.采用什么方法对共识协议的设计进行形式化验证、如何提升验证规模,是共识协议形式化验证的重要研究问题.对目前采用形式化方法验证共识协议的研究工作进行调研,总结其中提出的重要建模方法和关键验证技术,并展望该领域未来有潜力的研究方向.

摘要：为了解决Petri网对复杂软件系统进行形式化验证时在安全性描述、自动化程度和验证效率方面存在的不足,提出一种软件安全Petri网。扩展了库所定义,提出了安全距离及其计算方法,以增强Petri网对软件安全性的描述能力。设计了自动划分子网结合库所安全定级的递归算法,仅对与被验证需求性质相关的划分子模型进行验证以提高验证效率,同时实现库所的安全定级。设计并实现了软件安全性需求自动化建模和验证工具原型,最后给出了在典型安全关键软件———机载除冰软件系统上的应用以说明方法和工具原型的有效性。

摘要：为提高核电厂数字化仪控系统中HPD(HDL-Programmed Device)验证工作的效率和有效性,从而帮助提高仪控系统可靠性,引入形式化验证方法。形式化验证方法与传统的基于功能仿真的验证方法相比可以更有效地发现系统设计中的错误,更充分地验证系统设计,更方便地对验证流程进行管理。目前基于断言的形式化验证方法已经在大规模ASIC设计,以及数字通信领域HPD设计的功能验证中取得了成功,本文将这一方法引入核安全级系统HPD验证实践中,主要介绍HPD形式化验证的特点、原理和方法,以及其在FirmSys系统安全级HPD验证工作中的初步应用。

摘要：针对硬件安全验证的效率受形式化验证模型构建方式影响的问题,提出了一种面向硬件木马检测的自动构造形式化验证模型的方法。该方法首先遍历寄存器传输级设计的控制流图,提取出赋值语句的路径条件及其对应赋值表达式,构成Kripke结构中状态转移的约束关系;然后将Verilog语法的约束关系转换成模型检测器的语法,从而生成形式化验证模型;最后利用模型检测器对所构造的模型进行验证,当模型违反设定的安全验证属性时,检测到其中的硬件木马。利用Trust-HUB硬件木马测试基准的实验结果表明,该方法生成的形式化验证模型,能够有效检测寄存器传输级硬件设计中的木马。

摘要：Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义;其次设计了一组从离散事件模型到时间自动机的映射规则;然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal验证内核完成验证;最后,以一个交通信号灯控制系统为例进行了成功的转换和验证,实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.

摘要：采用模型检查技术,对IPv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的MSC(messagesequencecharts)来描述,并通过线性时序逻辑说明该协议的属性.还提出了由MSC模型的线性化自动抽取协议属性的方法.