军用指挥控制软件可信性分析与验证技术

随着武器装备信息化程度越来越高,军用指挥控制软件的可信性直接关系到装备整体效能的发挥。在对传统软件质量保证技术研究的基础上,结合军用指挥控制软件的特点,提出了基于形式化方法的软件分析与验证技术。分别从安全性质形式化规约技术、基于模型检验的指挥软件验证技术和基于静态分析的控制软件分析技术三方面保证军用指挥控制软件的可信性,最后,提出了适用于指挥控制软件全生命周期开发的形式化分析与验证集成环境。

潜艇腐蚀相关静态电磁场分布规律的实验验证

为对浅海环境中潜艇腐蚀相关静态电、磁场分布规律进行实验验证,根据场产生机理,提出对电场、磁场分布进行同步验证的实验方法,即同步测量水下2个深度平面上场源产生的标量电位及一条测线上的三分量磁感应强度,利用其中一个平面上的标量电位分布反演出场源参数,再据此预测另一平面上的标量电位及测线上的磁场分布,通过比较预测值与实测值,表明理论分析方法及结论的正确性.并在实验室中模拟三层平行分层浅海环境,借助潜艇缩比模型完成了上述实验验证过程,表明浅海中潜艇腐蚀相关静态电磁场分布规律的正确性.

利用Formal引擎提升复杂设计跨时钟域的检查和验证效率

为了减少复杂设计中可能的亚稳态风险,不少公司都采用工具或人工来检查设计中存在跨时钟域的问题。传统的检查方法只能检查设计中是否做了跨时钟域的处理,却无法检查处理得是否合理,而静态Formal验证技术采用数学穷举的方法,利用断言对设计中的同步器进行快速验证,确保数据的可靠传输,有效避免了一些设计缺陷。Mentor公司的Questa CDC和Formal工具可以对设计进行跨时钟域的检查,并可用Formal引擎证明设计中跨时钟域同步器与其断言的一致性,可极大地提高复杂设计的验证效率和鲁棒性。

SOC设计验证技术

本文论述了SOC正确性验证所使用的模拟、形式验证技术和静态验证技术等,并讨论了在设计过程中系统级、模块级、门级和物理级各个层次中的验证方法。

基于属性的形式验证技术及应用

为了提高产品的验证覆盖率和首次流片成功率,越来越多的验证技术和衡量标准被采纳。传统的仿真验证技术很难达到验证的快速收敛,而静态验证技术采用数学穷举的方法,利用断言对corner case进行快速验证,有效避免了一些设计缺陷。Mentor公司的Questa Formal工具可以对代码进行常规的功能检查,并可用Formal引擎证明设计代码及其断言的一致性,可极大地提高复杂设计的验证效率和鲁棒性。

台积电成功试产32nm静态随机存储器并通过功能验证

据报道，台积电1113在美国华盛顿特区举行的国际电子组件大会（IEDM）中发表论文，宣布开发出同时支持模拟及数字集成电路的32nm制程技术，并成功试产出32nm 2Mb SRAM，且已通过功能试验。

用DSP技术从模拟视频信号中获取数字图像

TMS320C6x11系列DSP以其高速的运算性能、充足的存储空间、独特的并行处理机制使得其在图像处理领域有着十分广泛的应用前景,因此有必要为其提供一套有效的图像获取方案。本文给出一套从模拟制式视频信号中获取数字静态图像的方案,具有通用性好、占用CPU时间少、实时性强等特点。经实际系统验证,本方案每秒钟可以稳定地获取720×576幅面彩色图像6.25幅,具有很好的实用性。

一种新的GPS静态多路径削弱方法

多路径误差是GPS的重要误差源之一。本文介绍了多路径效应产生的原理,归纳比较了目前国内外多种关于多路径误差的处理技术,论述了多路径效应的数学模型及其特性,提出一种通过移动平均来削弱GPS静态多路径的方法,通过实测数据进行分析,验证了其正确性。

融合句嵌入模型和代码特征的补丁验证方法

补丁验证常用运行测试套件的方法来验证补丁正确性,然而自动修复技术生成的补丁往往数量巨大,而将每个补丁依次通过测试套件则会产生难以承受的开销.针对该问题,本文提出一个由句嵌入模型InferSent和支持向量机分类器组成的静态补丁验证方法.使用InferSent提取代码静态特征并通过支持向量机分类器来预测补丁正确性.该方法更加关注代码的静态特征信息,通过对特征的提取分析,无需运行测试套件即可有效地预测自动修复工具生成的补丁的正确性.本文在多个自动修复工具生成的补丁集合上进行了验证.实验结果表明,在修复工具生成的补丁集合上,本文提出的静态补丁验证方法对补丁预测的F1值达到71.89%,相比其他两种最新静态补丁验证方法分别提高11.64%和6.43%,并在五项评价指标上均优于对比模型.表明该方法可以在不运行测试套件的情况下正确预测补丁,且具有良好的泛化能力.

电梯限速器静态拉力试验装置的分析

关于电梯限速器静态拉力的试验装置，在国内外电梯企业和监督检验部门都不是太重视。一方面是由于静态拉力不是符合限速器实际动作工况的验证方法，另一方面是由于研发技术含量普遍认为不高，所以一直以来都没有引起有关部门的关注。随着我国高速电梯的增多，使用的限速器速度提高以及种类的增多，限速器动态拉力试验要求变得具有一定的迫切性。作为限速器动态拉力试验装置的补充设备，推进限速器静态拉力试验装置的研究和开发进程是必要的。又因为限速器制造企业为了提高检验的速度和调试效率，也扩大了限速器静态拉力试验装置的使用范围。

美国完成先进的三级发动机点火试验

2010年3月25日，航空喷气公司和美国空军成功完成了先进的三级火箭发动机技术验证静态试验，试验是在加州爱德华空军基地的空军研究实验室进行的，验证的最大推力大于1438N。最初的试验结果表明，所有部件都按设计要求进行工作，所有性能都成功达标。

应用程序、专用程序、实用程序

Y2002-63279-165 0313060有规约编译器的应用形式验证=Applying formal veri-fication with protocol compiler[会,英]/Stangier,C.&Holtmann,U.//2001 IEEE Symposium on Digital Sys-tems Design.—165～169(TE)Y2002-63441-175 0313061防止未受权win32应用软件的执行=Preventing theexecution of unauthorized win32 applications[会,英]/Schmid,M.& Hill,F.//2001 IEEE DARPA Informa-tion Survivability Conference & Exposition,Vol.Ⅱ.—175～183(A)