MANET路由协议的正确性分析

移动自组网(MANET)是当前网络研究的一个热点,但是由于安全问题致使其未能广泛应用.在安全问题中,路由协议的正确性尤为重要.采用形式验证方法分析了MANET非安全路由协议和安全路由协议的正确性.首先给出了协议正确性的形式描述以及攻击者的形式定义,将协议的正确性分为安全性(Safety property)和活性(Liveness property),前者指协议所发现的路由具有某些良好的性质,后者指协议能够发现路由而且能够顺利地传输数据;然后提出了两个活性证明规则--响应性证明规则和反应性证明规则,并用所提出的活性证明规则在Isabelle/HOL中证明了DSR协议和SRP协议的正确性.     

船体几何造型设计及软件实现

叙述了船体几何造型设计软件功能、面向对象设计思想、软件系统分析与设计和系统运行环境，船体曲面造型设计软件是以消息驱动和具有图形用户界面的面向对象的软件系统。船体几何造型设计不同于传统的２Ｄ母型改造方法，它更接近于虚拟现实的设计概念，通过实船的３Ｄ船体几何型设计，证明本方法的正确性和软件系统的实用性。     

神经元计算芯片的VHDL算法级与RTL级模型的建立及模拟

本文针对神经元计算芯片的指令系统和体系结构，详细讨论了复杂电路的ＶＨＤＬ建模及模拟验证方法，分别给出了该芯片的算法级描述和ＲＴＬ级描述，并用相同的测试台对两级描述进行了模拟，验证了描述的正确性和功能的等价性。     

FORTRAN程序正确性的形式证明

本文描述如何利用程序正确性验证系统,形式化地证明 FORTRAN 程序的正确性。它为软件工作者提供了形式程序验证的模式,对提高软件产品的可靠性无疑有促进作用。     

蓝牙链路管理的系统级SOC设计方法

提出了事务级面向对象的设计流程TLOOF（Transaction Level Object Oriented Framework）,强调高层次的设计和验证,并使用面向对象的Petri网和实时UML相结合的方法,用System C对系统的行为建模．将TLOOF应用于蓝牙芯片的设计中,蓝牙行为模型由链路管理器和链路控制组成,映射为CPU、内存、片上总线、链路控制等体系结构模块．建立了蓝牙链路连接的OOPN模型并描述了事务级模型的类图,完成了系统的仿真．仿真结果表明,该片上系统（SOC）设计方法可以很好地对蓝牙系统建模．     

复杂星间链路网络规划评估方法

为确保以导航星座星间链路为代表的复杂星间链路的运行服务效果,在使用网络建链拓扑、路由规划参数前,应对其正确性和有效性进行评估确认.本文提出了对复杂星间链路网络规划进行参数正确性快速评估和业务服务性能评估的分级评估方法.第一级评估实现网络规划结果正确性的快速判断,涵盖了场景要素符合性、节点特性符合性、测量业务约束满足性、数传性能满足性等多维度综合化快速验证评估.第二级实现网络规划结果有效性的进一步确认,构建由星间网络行为模型和数据接入模型组成的星间链路网络仿真系统,基于星间数据传输和处理的加速仿真,统计建链数量和数据包传输性能并与业务服务指标比对,完成业务服务性能仿真评估.经对导航星座星间链路典型业务场景的两级评估结果的比对,验证了分级评估方法的有效性.     

用于系统级建模的DSP运算指令集设计方法

文章提出一种用于系统级建模指令集的设计方法并加以实现.该指令集作为某DSP的系统级设计建模和开发软件工具链的底层基础,为DSP的软硬件协同设计和软件模拟器的开发提供了一个平台.在工程化的测试中,通过该软件方法建立的DSP模型和硬件描述语言建立的DSP模型进行协同验证,证明了其正确性.     

一个描述内存工作区操作的公理语义方法

本文定义了一个内存工作区处理语言ＭＰＬ，并提出了用于描述语言的形式化方法，作为示例，文中最后给出一个程序部分正确性的验证提纲。     

PASCAL程序中FOR语句正确性验证

本文给出ｆｏｒ ｘ：－ａ ｔｏ ｂ ｄｏ ｓ语句正确性验证法则的推导，通过一实例说明这个法则的应用。类似地可给出ｆｏｒ ｘ：＝ｂ ｄｏｗｎｔｏ ａ ｄｏ ｓ语句正确性验证法则的推导。     

用HOARE逻辑证明C~( )程序的正确性

讨论了将HOARE逻辑应用于面向对象的程序设计语言C 程序的正确性证明的相关问题.如类的正确性以及软件系统的正确性     

一种函数分割型程序设计规范描述——FDP程序的正确性验证

FDP 是一种函数分割型程序设计规范描述手法。我们把按此法进行描述的设计规范叫作 FDP 程序。本文将提出实现 FDP 程序正确性自动验证的基本方法和具体步骤,以说明 FDP 的优越性。     

六层电梯模拟系统的研究与实现

本研究以模拟电梯实际运行情况为目的。首先,设计了控制电梯运行的调度算法;其次,采用面向对象语言编写程序模拟电梯运行,其中使用双缓冲技术来解决电梯图片在刷新过程中出现的闪烁现象;最后,测试本系统的正确性和合理性。     

基于环境的软件正确性形式化描述

软件的运行依赖于环境,在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中,其正确性是一个逐渐改进的过程,也就是说,通过不断地修改,软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素,本文将以三分之二互模拟为基础,利用网极限的观点,建立软件动态正确性的形式化描述。首先建立三分之二互模拟的无限演化理论,给出三分之二极限互模拟的定义。其次建立三分之二互模拟极限,这个极限在一定程度上反映软件规范是其实现的极限形式。最后证明三分之二互模拟极限与三分之二互模拟的相容性等性质。     

Excel中实现数据正确性的方法

Excel软件在统计、财务应用等领域使用非常广泛，这些领域的数据量很庞大，计算较复杂，如何保证数据的正确性是很重要的。本文介绍了Excel中几种实现数据正确性的实用、简单的方法。     

面向过程向面向对象程序设计的转变与实现

比较分析了面向过程设计思想和面向对象设计思想的区别与联系,并提出如何在教学中正确引导学生从面向过程设计到面向对象设计的自然过渡。     

模型驱动的Dafny程序形式化生成与自动验证

Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法; 然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式; 最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.     

浅析面向过程与面向对象

着重讨论了面向过程的程序设计方法和面向对象的程序设计方法，对面向过程方法和面向对象方法在分析过程、设计过程以及特点等多方面进行了分析和比较，从而得出面向对象的优点，并推荐使用面向对象的程序设计方法。     

智能CAA中基于语法树的程序正确性验证研究

基于语法树的程序正确性验证方法是目前程序正确性验证方面全新的研究领域,该方法以程序的语法树作为程序正确性的检验对象,运用适当的树匹配算法,来验证目标程序的正确性.文章在介绍基于语法树的程序正确性验证方法的基础上,借鉴了无序标签树匹配的相关研究成果,结合软件构件的查询技术,提出了一种新的XML路径查询模型和树匹配算法,在理论和方法上对这个方法的实现进行了初步探讨,并结合XML技术提出了一套实现这一方法切实可行的解决方案.     

面向对象软件测试探讨

面向对象软件测试是面向对象软件开发的不可缺少的一环，是保证软件质量，提高软件可靠性的关键．但目前的研究现状与面向对象的分析、设计技术以及程序设计语言的研究相比尚显薄弱．本在分析面向对象程序设计语言对软件测试影响的基础上，讨论了面向对象软件测试的测试策略及测试技术．     

结构化与面向对象的程序设计方法比较

程序设计的基本方法包括早期的结构化程序设计方法和面向对象的程序设计方法.从程序设计的角度看,结构化方法和面向对象方法各有优缺点.从提高程序的重用性和可维护性的角度看,面向对象方法有较好的应用前景.但面向对象程序设计方法的基础仍然是结构化程序设计,即由顺序、分支与循环三种结构来组成.因此,对于程序设计人员来说,应首先掌握结构化程序设计方法,在此基础上掌握面向对象程序设计方法.