一类循环条件非线性的程序终止性

针对Tiwari提出的线性循环程序的终止性判定问题,提出了循环条件为齐次多项式的非线性程序的不可中止性判定的理论证明,然后将程序终止性判定问题转化为参数半代数系统的求解。在求解中,借助强有力的代数符号工具DISCOVERER,解决了计算机浮点计算所造成的近似误差,精确地判定这类程序的不可终止性。最后,通过计算代数理论,把循环条件推广到了非齐次多项式,并且进行了验证。通过理论的证明和实验的验证,解决循环条件是非线性的一类循环程序的方法是高效合理的。     

程序正确性验证的代数方法及其研究进展

程序的完全正确性包括程序的部分正确性和终止性,为了提高程序验证的正确性,介绍了程序正确性的验证方法,包括基于公理化验证程序的完全正确性,基于不动点定理、特征值理论、秩函数、有限差分等验证程序的终止性.最后,总结了各种验证方法的研究现状以及未来发展.     

（2＋1）维非线性耦合可积广义Kaup方程的精确解

应用截尾辅助函数法,借助计算机代数系统与符号计算,获得(2 1)维非线性耦合可积广义Kaup方程若干显式精确解,其中包含周期解和孤立波解.     

概率带测试克林代数操作语义的研究

为了增强带测试克林代数 (KAT) 的表达能力,提出了一种加概率的带测试克林代数 (PKAT) 的理论,并将其应用于对加概率正则程序的推演.将概率格局变迁系统作为操作语义的模型,它的每个状态是一个格局,格局是由一个 PKAT表达式和一个数据状态组成的序列对.为了确立模型中的关系,定义自然语义和结构操作语义,均从行为和状态两方面进行刻画,证明两者在只考虑程序正常终止的情况下是等价的.     

非线性循环及Rm上线性循环的终止性判定

为了研究程序设计中的软件可信性问题,分析了非线性单重循环程序Whilex∈Ωdo｛x:=f(x)} end当Ω为有限个互不相交的闭区间之并时的终止性,证明该终止性在一定条件下可以由周期轨道的存在性加以判别,给出了确定条件下此类程序不终止的充分必要条件,并建立了相应的判定程序.进一步,利用Brower不动点定理及凸分析的理论,在Rm上建立了当循环条件Ω是有限个互不相交的闭凸集之并时线性循环程序终止性判定的方法.     

基于双曲函数法的五阶非线性演化方程显示行波解

利用双曲函数方法对Mikhauilov-Novikov-Wang方程的约化情形进行了研究。通过行波约化,将五阶非线性演化方程转为成一个ODE。结合Riccati方程的性质,得到一个关于若干参变量的代数系统,借助于Mathematica符号计算功能,最终得到了上述方程的显示行波解,包括类孤子解、三角函数周期解和有理解。     

带有规则优先级的主动规则终止性分析

主动规则的终止性指规则集的规则之间的相互触发不会无限循环下去,即规则是可终止的。对主动规则的终止性分析方法包括图方法和代数分析方法。针对已有分析方法的局限性,介绍一种主动数据库规则终止性分析的一种新方法,将主动规则翻译成逻辑语句,考虑到系统的执行语义,转换为演绎规则中已知终止性的主动过程,利用该规则终止性分析方法对更多规则进行终止性分析,给出相应定理及其证明,最后给出规则优先级算法。     

耦合KonopeIchenko-Dubrovsky方程的新精确解

利用一种基于符号计算的代数方法,结合Maple环境中的Epsilon软件包,求解耦合Konopelchenko—Dubrovsky方程,获得了新的显式行波解,其中包括Jacobi椭圆函数解、双曲函数解和三角函数解。用F-展开法求得（2＋1）维色散的长波方程的新周期波解和孤波解。     

基于关系查询的应用系统向语义网移植的研究

针对基于关系数据库的遗留系统能否集成到语义层这一问题,研究关系查询到语义查询转换的完备性.分析一种从关系数据库获取本体的自动学习方法,抽取数据库表、属性同本体类、属性之间映射函数.基于这些函数,得出关系对应的基本简单协议和RDF查询语言(SPARQL)代数表达式.逐一用SPARQL代数来模拟5种基本关系代数运算:选择、投影、并、差和笛卡尔积,并给出其相应的转换算法.结果表明:在这种本体学习的方法下SPARQL代数可以表达5种基本关系代数,以及由它们组合而成的关系表达式,因此,SPARQL是关系完备的,并支持那些基于关系查询的遗留系统向语义层的移植.     

关于循环终止性证明的一种最小不动点方法

本文分析了循环终止性的特点,给出了实WHILE语句模型,简要地叙述了最小不动点理论,并结合到实循环函数上讨论了终止性的证明。     

线性半代数变迁系统的近似互模拟等价

针对软件程序状态间转移关系存在不等式约束的问题,给出一种形式化的程序描述系统,即线性半代数变迁系统。在该系统的基础上,为简化软件程序结构,采用特征列的方法,提出了基于线性半代数系统共同零点的互模拟等价概念及计算方法。但在工程应用中大多数实验所得数据仅为给定误差范围内的近似值,精确的系统等价关系缺乏容错性及灵活性。为获得更恰当的系统关系,利用奇异值分解对系统进行近似处理,建立了系统的近似互模拟等价概念及计算方法。通过符号与数值混合计算,实现误差可计算及可控制。最终选取近似等价系统代替原复杂系统。并发通信程序中的实例分析表明,该方法在简化软件程序设计中具有合理性及有效性。     

C语言程序结构自动分析器的设计与实现

为了对用C语言编写的大型软件系统的程序结构进行自动分析,我们设计了一个C语言程序结构的自动分析器。本文给出了其设计思想,实现方案,并简要地说明了它的功能和使用方法。     

基于场景的并发系统需求验证方法研究

为验证并发系统需求设计的正确性,提出一种基于场景的并发系统需求验证方法.首先,用UML顺序图建模并发系统需求场景,通过定义顺序图的操作语义及转换规则,将顺序图的XML描述文件自动转换为Promela程序,而后将描述系统需求的Promela程序和描述系统规约的线性时序逻辑作为模型检测器SPIN的输入,用模型检测的方法自动...     

基于MSCA的符号网络函数模拟器

提出了一种改进的用于产生模拟电路符号网络函数的符号编码算法MSCA。与原符号编码算法(SCA)相比,该算法具有更简洁的编码单元,更为准确的编码定理,从而能明显地提高算法的效率和应用范围。基于MSCA用于模拟电路的符号网络函数模拟器SNSAC已经开发完成,还介绍了SNSAC的基本结构和特点。最后给出了程序应用的两个例子。     

符号网络分析算法及计算机实现

提出了一种分析电路符号网络函数的新编码算法NSCA。它能有效降低基码,防止过早发生整数溢出,从而扩大分析电路的规模。提出了灵敏度分析算法和化简算法,并可对模块电路进行处理,增强了编码算法的适用范围。根据该算法开发了软件系统SNSPC2.0实例运行结果证明了算法理论的正确性和可行性。     

计算机生成符号网络函数的有效算法

K.Singhal 和 J.Vlach 以摄动理论为基础生成符号网络函数的方法是十分有效的。本文给出了这一算法的新的证明,使理论和推导过程得到很大简化。同时给出了计算以元件值增量定义的符号网络函数和以元件值定义的符号网络函数的统一的公式。     

规则波形的智能理解方法

本文提出了一种波形的符号描述方法,该方法的实现便于诊断专家系统从规则波形中自动获取故障知识.文中讨论了如何将规则波形用波元符号来表达和基于这种符号表达的波形局部畸变特征的谓词描述,并讨论了基于深知识的发动机点火波形的理解,从而获取状态知识的过程.     

数字示波器自动检定方法与实现

利用开发的专用软件,通过接口连接控制9500B示波器校准仪与各类数字示波器,建立了数字示波器自动检定系统,实现了数据录入、数据处理、合格与否的判断、检定证书的生成等功能的自动化,同时支持对示波器单个参数的检定。该检定系统提高了计量检定的自动化水平,不但使检定效率至少提高4～6倍,而且降低了人员操作和数据录入失误造成的差错率。     

一种虚拟化恶意程序检测系统的实现

为了自动智能检测出新变种的恶意程序,使用虚拟执行与应用程序接口钩子技术,分析程序执行中调用的系统接口,将接口调用顺序编码形成一个特征序列。运用编辑距离算法计算程序特征序列与数据库中恶意特征序列的相似度,实现自动判别恶意种类的功能。在随机选取样本的的前提下,本系统对样本分析后结果表明,检测识别精确度达到92%,误报率仅为6%。     

基于符号模型检验的可信跨域协作系统验证方法

针对规范调控的可信跨域协作系统属性验证的困难,提出一种基于符号模型检验的可信跨越协作系统验证方案.该方案包括规范语法及其状态语义、系统抽象模型、验证算法三大部分.其中规范的状态语义是方案的核心,它将规范集映射为其所对应的状态或状态转移集,消除了系统模型和规范的语义不一致性;系统抽象模型包括规范Kripke结构和路径规范性定义,以及规范Kripke结构的分支时态逻辑（CTL）语义3个部分,实现了可信系统的形式建模;验证算法描述了系统符号模型检验的具体实现过程.与基于定理证明的验证方案相比,该方案有效降低了验证时间,提高了验证效率.