RELAP/SCDAPSIM/MOD4.0程序的FHR应用扩展及验证

基于轻水堆最佳估算系统分析程序RELAP/SCDAPSIM/MOD4.0,添加新的FLi Na K熔盐热物性参数和适用于熔盐的对流换热系数,开发了适用于FHR系统的热工水力分析程序RELAP5-FHR。通过FLi Na K高温熔盐实验回路对RELAP5-FHR程序进行实验验证。结果表明:RELAP5-FHR程序计算值与实验值吻合较好,验证了程序的适用性。     

嵌入式实时操作系统内核混合代码的自动化验证框架

"如何构造高可信的软件系统"已成为学术界和工业界的研究热点.操作系统内核作为软件系统的基础组件，它的安全可靠是构造高可信软件系统的重要环节.为了确保操作系统内核的安全可靠，将形式化方法引入到操作系统内核验证中，提出了一个自动化验证操作系统内核的框架.该验证框架包括：（1）分别对C语言程序和混合语言程序（C语言和汇编语言）进行验证；（2）在混合语言程序验证中，为汇编程序建立抽象模型，并将C语言程序和抽象模型粘合形成基于C语言验证工具可接收的验证模型；（3）从规范中提取性质，基于该自动验证工具，对性质完成自动验证；（4）该框架不限于特定的硬件架构.成功地运用该验证框架对两种不同硬件平台的嵌入式实时操作系统内核μC/OS-II进行了验证.结果显示：利用该框架在对两个不同的硬件平台上内核验证时，框架的可重复利用率很高，高达到88%，虽然其抽象模型需要根据不同的硬件平台进行重构.在对基于这两种平台的操作系统内核验证中，分别发现了10~12处缺陷.其中，在ARM平台上两处与硬件相关的问题被发现.实验表明，该方法对不同硬件平台的同一个操作系统分析验证具有一定的通用性.     

Windows x64无签名驱动程序运行方法

主机监管系统利用过滤驱动程序对系统实现全面监管.随着微软64位操作系统的推出,要求驱动程序经过付费签名后才能正常运行.由种种原因使驱动程序不能被签名时,主机监管系统就不能在WINDOWS 64位操作系统上使用.因此无签名驱动程序问题成为在WINDOWS 64位系统开发最普遍的问题之一,会导致程序难移植、影响用户体验.通过对WINDOWS 64位系统数字签名过程的逆向分析,提出一种能一次性关闭系统数字签名验证机制的方法,从而顺利加载运行未签名驱动程序.     

基于交互式定理证明的并发程序验证工作综述

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

采用CPAChecker的动态程序验证

针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法. 首先,根据程序的控制流程图,对程序进行静态检测。 在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检测的过程。 其中,抽象检测可以有效地限制系统模型的规模,动态执行不仅可以有效地减少静态检测导致的误判,而且有助于引导构建精确的系统模型,降低虚假反例的数量和不必要的反例分析和精化。 实验数据显示,这种算法明显提高了传统的反例引导谓词抽象精化算法的检测效率和准确率。     

基于前后断言法的温度控制系统程序验证

温度控制系统已经广泛地应用于各个领域,温度控制系统对可靠性要求较高,一般来说,温度控制系统的故障将导致灾难性的后果。温度系统的设计直接影响了系统的可靠性,文章利用前后断言法对温度控制系统的设计进行验证,结论表明,该方法可以保证温度控制系统设计的正确性,保证系统可靠运行。     

电路板雕刻过程中的刀路生成与规划

首先分析了电路板的常用制作方法,然后介绍了一种既能减少污染,又能保证加工精度与效率的基于物理雕刻的电路板雕刻机系统.主要对电路板雕刻过程中的刀路生成作了详细论述,并在采用环切与行切相结合的加工方法的基础上,提出了一种基于电路板雕刻的行切刀路规划算法,最后用VC 编写了相应的程序,经程序验证此算法准确可靠,能够满足电路板的加工要求.     

XYZ系统在电信领域中的应用

最近几年，在软件工程界内部有一种趋势，这就是开发以面向具体领域的ＣＡＳＥ环境．作为这样的一种ＣＡＳＥ工具，ＸＹＺ系统是由一时序逻辑语言ＸＹＺ／Ｅ和一组基于该语言的工具集构成．在ＸＹＺ系统中有很多的工具，它们被用来满足不同的需要．众所周知，ＳＤＬ（ｓｐｅｃｉｆｉｃａｔｉｏｎａｎｄｄｅｓｃｒｉｐｔｉｏｎｌａｎｇｕａｇｅ）是电信领域中的一个国际标准语言，而且有关基于该语言的环境已在开发，但是有关该语言的验证工作，特别是利用有关时序逻辑语言进行验证的工作还不多．作为一种尝试，本文将利用ＸＹＺ系统中的一个子系统ＸＹＺ／ＶＥＲＩ，对ＳＤＬ所描述的有关电信领域中的例子进行验证．     

LFM-CW雷达信号处理算法研究及仿真

从理论上对LFM-CW雷达进行信号分析,并对LFM-CW雷达的信号处理方法进行简单研究,最后通过仿真程序验证了该信号处理方法(距离/多普勒处理)在计算运动目标距离和速度时的正确性,为LFM-CW雷达信号处理提供了理论依据.     

关于程序验证方法的讨论

一、引言 自从1967年Floyd发表其论文“给程序赋予意义以来,程序自动验证工具的研究持续了数十年。Floyd在文[4]中提出了用“断言式方法”证明程序的正确性。其具体作法是:在程序程图的每一条