基于半空间的最短路径算法模型研究

目前在GIS领域,对最短路径搜索问题的研究和应用较多,其中最短路径搜索算法的效率问题是普遍关注和在实际应用中迫切需要解决的问题.通过对基于Dijkstra最短路径搜索算法的优化途径的分析,提出了基于半空间的最短路径算法,并在VC 环境下设计相应的程序验证了此算法.应用该算法开发了"焦作市地理信息公共查询系统"系统,取得了比较满意的效果.     

导航接收机上位机软件的设计与开发

本文以GPS导航接收机的研制为背景,在VC MFC AppWizard环境中针对上位机软件进行了详细的说明,其中包括上位机与下位机之间的数据通信、数据的实时显示、实时绘图、线程的使用、用户界面的设计等等.重点介绍了软件在开发过程中的要点和难点.其后,通过与下位机连接,运行GPS导航接收机程序验证了上位机软件开发的正确性、实用性、直观性.     

常用循环摘要的自动生成方法及其应用

采用形式化方法证明软件的正确性是保障软件可靠性的有效方法,而对循环语句的分析与验证是形式化证明中的关键,对循环语句的处理一直是程序分析与验证中的一个难点问题.本文提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果,并将该执行效果定义为循环摘要.同时,本文提出了一种自动生成循环摘要的方法,可以为操作常用数据结构的循环自动生成循环摘要,包含嵌套循环.此外,基于循环摘要,我们可以自动生成循环语句的规约,包括循环不变式、循环的前置条件以及循环的后置条件.我们已经实现了自动生成循环摘要以及循环规约的方法,并将它们集成到验证工具Accumulator中,实验表明,我们的方法可以有效地生成循环摘要,并生成多种类型的规约,从而辅助软件程序的形式化证明,提高验证的自动化程度和效率,减轻验证人员的负担.     

基于分离逻辑的程序验证研究综述

上世纪60-70年代以来,虽然有Floyd-Hoare逻辑的出现,但是使用形式化工具对命令式程序的正确性和可靠性进行自动验证一直被认为是极具挑战性、神圣不可及的工作.上世纪末由于更多的科研投入,特别是微软、IBM等大型公司研发部门的大量人力物力的投入,程序验证方面在本世纪初取得了不少进展,例如用于验证空客代码无运行时错误的ASTRÉE工具,用于Windows设备驱动里关于过程调用的协议验证的SLAM工具.但这些工具并没有考虑动态创建的堆（Heap）：ASTRÉE工具假设待验证代码没有动态创建的堆,也没有递归;SLAM假设待验证系统已经有了内存安全性.事实上很多重要的程序,例如Linux内核、Apache、操作系统设备驱动程序等等,都涉及到对动态创建堆的操作.如何对这类操作堆的程序（heap-manipulating programs）进行自动验证仍然是个难题.2001-2002年分离逻辑（separation logic）提出后,其分离（separation）思想和相应的框（frame）规则使得局部推理（local reasoning）可以很好地应用到程序验证中.自2004年以来,基于分离逻辑对操作动态创建堆的程序进行自动验证方面的研究有了很大的进展,取得了很多令人瞩目的成果,例如SpaceInvader/Abductor、Slayer、HIP/SLEEK、CSL等工作.本文将着重对这方面的部分重要工作进行阐述.     

循环条件的形式化推导在程序验证中的应用

提出了一种求解命令式程序中循环执行和终止条件的方法.该方法基于循环代码本身进行循环执行和终止条件的分析推导,可以定义一个原型工具进行自动化推导.现有的形式化方法依赖于形式化规范,而提出的方法适用于未被形式化的程序.提出的形式化方法可以在一个原型工具中实现,通过该工具来推导循环执行和终止条件,辅助程序验证和程序缺陷修正.     

基于QBF的循环不变式构造技术

构造循环不变式是程序验证的核心问题之一。主流的循环不变式构造方法通常假设程序中的变量在无限数域上取值,然而程序执行过程中变量都是用有限长度的位向量来表示,无限数域上的循环不变式在有限数域的程序中可能不再是不变式,反之亦然。针对这一问题,本文给出一种基于QBF求解的构造有限数域上循环不变式的方法。该方法可用于构造类型丰富的不变式,包括线性(或多项式)等式(或不等式)不变式,支持加、减、乘、除、移位、位操作等,允许不变式中出现量词。本文也例证了该方法在程序终止性证明、循环上界分析、程序正确性证明等方面的应用价值。     

HTR-10一回路流量变化试验的模拟

10 MW高温气冷实验堆(HTR-10)是我国第一座高温气冷堆。一回路流量变化试验是HTR-10的三个动态特性试验之一,该试验不仅证明了反应堆的功率自调节性能,也为系统分析程序的验证提供了实测数据。基于实际的试验工况,利用THERMIX程序对一回路流量变化试验进行了模拟,分析了反应堆主要参数的变化。关于反应堆功率,计算结果与试验结果符合得很好,证明程序能够满意地再现HTR-10在该试验中的动态特性。试验过程中,燃料元件中心最高温度始终低于1 230℃的温度限值。     

国际标准题51“公开测试”阶段进展及分析

为验证热工水力程序对失水事故条件下非能动核反应堆行为的模拟能力，并评估最佳估算程序预测特定实验的能力，基于我国大型整体效应试验台架——先进堆芯冷却系统机理实验（ACME）台架，经济合作与发展组织核能署组织开展了国际标准题51号（ISP-51）项目。针对目前公开测试阶段已提交的程序计算结果，进行初步对比分析，结果表明，对于同一冷管段2英寸小破口失水事故，华中科技大学、西班牙加泰罗尼亚理工大学使用的热工水力最佳估算程序RELAP5，其模拟结果在非能动安全系统触发时间、流量值等方面与实验值较为吻合。而马德里理工大学、西班牙NFQ公司使用的TRACE程序，在其模拟结果中，各非能动安全系统触发时间均有延迟，ADS1~3气液流量明显高于实验值，可能与不同临界流模型的选取及阀门管线设置方式相关。该项目开创了由经济合作与发展组织非成员国发起和负责国际标准题项目的先例，有助于我国相关科研团队进一步熟悉国际核科技研究合作项目的运作及组织管理，在国际核能科技合作中承担更多工作。      

循环不变形状图的自动推断

在指针程序的分析和验证过程中,循环不变式的自动推断一直是个研究热点.文章首先介绍所提出的形状图和形状图逻辑,形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑.然后在此基础之上,设计了一种基于形状图逻辑的形状分析方法,并提出了一种基于形状图逻辑的循环不变形状图的推断方法.