可能性测度下计算树逻辑的若干性质

为讨论可能的计算树逻辑(PoCTL)与计算树逻辑(CTL)的关系,给出PoCTL公式与CTL公式等价的概念,利用公式的等价性证明了CTL是PoCTL的一个真子集.通过PoCTL模型检测算法与PoCTL公式的分析,解决了PoCTL模型检测的时间复杂度问题.最后对重复事件与持久性事件的定性性质及定量性质进行研究,用实例验证了CTL公式与PoCTL公式在可能性测度与概率测度下的本质区别.     

命题投影时序逻辑并发建模与自动验证

针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性判定算法,证明了命题投影时序逻辑统一框架模型检测是可判定的,从而得到了其自动验证方法,并给出了一个验证实例.     

温控系统的π-演算的描述与验证

根据温控系统的特征以及需求说明,利用π-演算构建了该系统动态行为的交互模型,依据π-演算的反应规则仿真描述模型的行为交互过程,使用μ-演算和移动工作平台(MWB)工具分析和验证了该交互模型具有温度控制和阈值修改功能,从形式上证明了温控系统的需求说明及其π-演算模型的一致性。结果表明,π-演算能够清楚地描述和分析并发系统的行为交互,而μ-演算可以证明模型的有效性和正确性。     

在数字电路验证中使用模型检验

形式化方法作为仿真方法的补充,为电路功能验证提供了新的途径.介绍了形式化验证方法之一,模型检验的理论基础和实现方法.介绍了分支时态逻辑CTL、CTL的固定点算法,二元决策图BDD,以及符号模型检验方法.最后使用SMV工具在一个CISC处理器的存储管理单元(MMU)上应用了模型检验,验证了模型检验在模块级验证中的可行性.     

PPTL模型检测器实现的一个关键技术

针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效迹数目,有效地实现PPTL模型检测.     

Jacobi猜想的逻辑化约

提出有关Jacobi猜想的两个命题:A.若Janobi猜想在有理数域Q上成立,则Jacobi猜想在代数域Q上成立.B.对每个正整数对(n,d),存在正整数f(n,d)使得:对每个素数p>f(n,d)及每个特征数p的域K,若多项式映射F:K~n→K~n适合degF≤d且detJ(F)=1,则F可逆.然后用模型论方法证明了定理:“命题A与B成立”等价干“Jacobi猜想对一切特征数0的域成立”.     

异构服务聚合的协同访问控制算法研究

由于服务聚合要实现异构多态交互过程,必然对安全访问控制模型的性能提出较高的要求.为满足服务聚合的访问控制需求,本文提出了一种异构服务聚合协同访问控制算法ACAHSP.首先,本文剖析了服务聚合中访问的动态情景要素构成,从多维度定义了构成情景的不同要素;然后,提出了基于动态情景状态的状态演算和规则演算的机制,并给出了动态情景机约束下在服务聚合模型ACAHSP;其次,基于CP ABE算法提出了ACAHSP访问控制模型的安全验证算法,强有力的保证了ACAHSP模型在服务聚合中访问控制机制状态机转换、数据交互的安全性;最后,结合案例进行应用验证,并与已有模型进行对比.     

测控技术中含有"X"值的验证

利用模型检验技术来验证具有“X” （未知）值的属性.给出了三值（真、假、未知）逻辑公式的模型检验算法,此算法与二值逻辑模型检验算法相比,并没有增加时间复杂度.通过实例说明三值逻辑模型检验算法的应用.     

命题公式真值表的生成与公式类型的机械判定

在文[1]的基础上,给出了命题逻辑中任一命题公式的真值表的生成算法与命题公式类型的判定算法,实现了利用计算机对有限多个命题公式的真值表的直接计算和输出,以及对一个命题公式是重言式、矛盾式或可满足式的机械判定.     

关于复合求积公式余项的研究

借助积分相关理论,给出了数值积分中复合梯形公式和复合Simpson求积公式余项误差事后估计式的严格证明及其余项表达式中的导数因子f″(ηn),f″(η2n),f(4)(ηn)和f(4)(η2n)在n充分大时的变化情况.为处理求积公式余项关系式提供了新的方法.     

基于LSC模型检验的性质抽取

采用LSC(live sequence chart)描述基于场景的需求规格说明,根据设计模型必须满足需求规格说明的一致性原理,针对安全性、可达性、活性等性质,设计3种用于自动生成和抽取性质的覆盖准则,并根据准则从LSC需求规格说明中抽取与设计模型相关的性质.抽取的结果可用于自动化验证,为验证需求模型与设计模型的一致性提供保障.     

与Gauss-Turán求积公式有关的极小值

对于给定的权函数 dμ(x) ,若存在 n次首 1多项式 P*n (x) (称为 s-正交多项式 )使下列积分F(s,μ) =∫R[Pn(x) ]2 s+ 2 dμ(x)达到极小 ,Pn(x) =xn +an- 1 xn- 1 +… +a1 x +a0 ,则以多项式 P*n (x)的 n个不同零点 x1 >x2 >… >xn- 1 >xn 作为节点的下列求积公式 (称为 Gauss-Turán求积公式 )∫Rf (x) dμ(x) =∑2 sj=0 ∑nk=1Ajkf ( j) (xk) +E2 s,n(f ) .具有代数精确度 2 (s+1 ) n -1 .但我们对 F (s,μ)所知不多 .Milovanovic′在他最近的一篇文章里提出计算 F(s,μ)的值 .本文主要解决了若干权函数下的上述极小值问题     

一个算术函数与最大素因子函数的β次混合均值

对任意正整数n,通过对Smarandache可乘函数f(n),因子积数列Pd(n)及除数函数d(n)进行构造,并利用初等方法及素数分布的性质对建立的∑n≤x(f(P_d(n))-1/2d(n)P(n))~β的混合均值问题进行研究,给出了一个较强的渐近公式.     

计算机代数在有限群同构类计数中的设计与应用

文献[1]论证n阶群同构类的个数在1000以内的存在性。文章给出群同构类Balass计数公式运算的算法,用计算机代数语言Matlab加以实现,进而将群同构类的个数推广到3000。即设f(n)为n阶群同构类的个数,证明方程f(n)=k,(1≤k≤3000)解的存在性。     

一种基于模型检验的类测试用例生成方法

提出一种新的自动生成类测试用例的方法.使用符号执行从类源代码抽取对象的状态和行为,以一个四元组抽象描述类,并转化成等价的Kripke结构.使用CTL公式描述测试覆盖标准,然后把这组CTL公式和描述类状态行为的Kripke结构输入模型检验工具,并利用模型检验工具自动生成相应的证据路径,最后将路径转化成满足相应覆盖标准的类测试用例.该方法直接从源代码生成测试用例,并使用贪心法约减冗余用例以降低测试成本.实验表明该方法生成的测试用例具有较高的覆盖率.     

一种基于快速阵列算法实现的IIR数字滤波器

为了对普遍存在于电子系统和通信系统中的有源噪声进行控制,提出了一种基于快速阵列算法实现的IIR数字滤波器.在对基于传统RLS算法实现的IIR滤波器深入分析的基础上,通过把次级通道的传递函数与回归向量ψf(n)结合起来,并从回归向量ψf(n)的数据结构出发,把回归向量分解为滤波器的先前输出采样ψ1f(n)和参考信号采样ψ2f(n);通过保范映射和内积矩阵形式,最终得到用于滤波器系数更新的阵列形式;同时还比较了2种算法的计算复杂度.仿真结果表明,提出的快速阵列算法不仅降低了计算复杂度,而且对有源噪声信号的相消控制,其收敛速度相对于基于传统RLS算法的收敛速度快大约46%.     

线性分式的自迭代周期

考虑一种特殊的线性分式 f( x) =x- 1x+ d,证明适当选择常数 d,可以得到自迭代周期等于n( n≥ 3)的线性分式 ;并给出矩阵形式的等价命题 ,通过矩阵运算 ,利用复数性质 ,得到 d的表达式 .     

物联网服务的π-演算建模与验证

针对物联网服务建模和验证问题,用π-演算理论对物联网服务和环境实体进行动态交互行为建模,并引入μ-演算刻画物联网服务能力,将其描述为物联网服务和环境实体动态交互行为的执行序列。针对特定的应用场景,使用π-演算定义了物联网服务和环境实体,利用μ-演算对物联网服务能力进行建模,使用检测工具MWB验证了模型的安全性、活性和时间约束三个性质,为物联网服务建模和验证提供了参考。     

Combinator演算族的π演算语义

以SKI演算作为Combinator演算族的代表, 通过形式化的手段给出了SKI演算的π演算语义; 通过一个实例验证了所论方法的正确性. 所给出的转换方法证明了π演算的表达能力： π演算为图灵完备的. 由于高阶函数式语言与Combinator演算族之间存在着自然的转换, 所给的转换思想不仅为在π演算的理论框架下 研究Combinator演算族提供了基础, 也为探讨高阶函数式语言的表示和实现问题提供了新途径.     

一种单输入/单输出的小脑模型神经网络研究

针对标准小脑模型关联控制器（CMAC）存在的问题,研究了一种单输入单输出（SISO）的CMAC算法.SISO CAMC采用直接地址映射,以输入v的量化值为地址,建立起输入v与权重w的关系,并通过对输入v进行归一化,增强网络的泛化能力.另外,学习采用随机样本,具有学习简单、收敛速度快、函数逼近精度高等特点,可以在单片机上实现.最后,理论证明和仿真试验,验证了该算法的有效性.