具有可和系数中立型时滞差分方程的振动性与正解的存在性（英）

考虑如下形式的线性中立型时滞差分方程△(Xn-PnXn-k)+qnXn-l=0,n=0,1,2,……其中{Pn}、{qn}均为实数列且Qn≥0,k,l为非负整数.在允许Pn-1振动情况下,本文建立了该方程所有解振动性和正解存在性的几个新的充分条件,其中不需要文献中通常用到的发散条件 qn=∞,作为应用,证明了方程△[xn-esin xn-4k]+ceβn-1=0,c＞0所有解振动的充要条件为β≤ .     

多速率混合系统的符号化可达性分析

针对目前还没有专门的数据结构处理多速率混合系统的符号化可达性问题，定义了多速率区域来表示和处理多速率自动机的无穷状态空间，从而把多速率混合系统的符号化可达性分析等价地转化成多速率区域上的3种操作，即并操作、变量重赋值操作和控制状态上的时间流逝操作．从理论上证明了多速率区域在这3种操作上的封闭性，同时定义了矩阵数据结构不同上限矩阵（DCM），并用其存储多速率区域，这样就得到了一种专门处理多速率混合系统符号化可达性分析的数据结构．理论上证得，DCM可以大大降低可达性分析算法的复杂度．     

分数阶金融模型的混沌控制

本文运用时滞反馈控制策略研究了一类分数阶金融模型的混沌控制问题,通过分析受控系统的特征方程,建立了系统稳定和Hopf分支存在的充分准则.设计的反馈控制器能有效地抑制系统的混沌行为.数值模拟证实了理论分析的有效性.     

面向命题投影时序逻辑的安全协议模型检测

针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.     

利用投影时序逻辑的多内核进程调度建模与验证

针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公式P,在PTL公理系统的基础上,通过证明S蕴含P是否为一个定理来验证系统是否具备该性质.以2内核处理器上的多级反馈队列算法的正确性为案例进行检验,结果表明所提方法可验证多内核处理器进程调度的系统性质,保证多内核进程调度的可靠性.由于多内核处理器的进程调度具备了并发系统的主要特点,因此该方法也适用于一般的并发系统验证.     

临界状态下中立型时滞差分方程解的振动性

考虑中立型时滞差分方程　　△ (xn-pnxn-k) qnxn-l =0 ,n =0 ,1,2 ,… ( )其中pn,qn(n =0 ,1,2 ,… )是实数且pn≥ 0 ,qn≥ 0 ,k和l是非负整数 ,获得了临界状态下方程 ( )所有解振动的一个充分条件 .     

具有无界时滞的泛函微分方程解的振动性

运且一种有效的方法研究一类形式广泛的泛函微分方程解的振动性，得到了Ｈｕｎｔ－Ｙｏｒｋ型定理的一般形式，推广了一系列已有的结论。     

临界状态下中立型时滞微分方程解的振动性

讨论了一类中立型时滞微分方程所有解的振动性,获得了临界状态下该方程所有解振动的一个充分条件。     

正整数分拆数的一个递推公式

本文给出了计算正整数分拆数的一个递推公式: a_n~h=sum from i=h to [n/2] a_(mj)~i+1 (1≤h≤[n/2]) a_n~h=1 ([n/2]相似文献   

应用UML2.0模型的测试用例生成方法

针对软件开发过程中测试自动化程度低的问题,在研究基于模型的测试用例生成技术的基础上,提出了一种基于UML2.0序列图与用例描述的测试用例生成方法.采用事件确定有限自动机来描述系统序列图,通过命题投影时序逻辑的模型检测技术,验证了自动机模型的正确性.使用自动机模型与用例描述来生成测试用例,该用例满足事件与全路径覆盖准则.通过对图书管理系统的分析表明,该方法不仅能够提高软件的测试效率,而且还确保了针对管理员的执行动作所产生的测试用例的正确性.