过程提取用于改善程序模型检测的可伸缩性

针对目前基于谓词抽象的程序模型检测工具很难处理大规模软件的现状，提出用过程提取技术对待检的源代码进行预处理，以改善程序模型检测的可伸缩性．首先，将程序中一个选定的语句集合提取出来并包装成一个独立的过程，然后在原程序的相应位置用一个过程调用替代，进而将大型程序分解成语义一致的小型过程的集合．由于模型检测算法中的过程总结边可单独计算，所以过程提取使整个程序的模型检测任务模块化，当程序对某过程进行多次调用时，利用总结边可以避免对过程体内状态空间的重复搜索，从而降低了模型检测算法在空间：和时间上的开销．理论分析和实验表明，所提技术能有效缩短大型程序的模型检测时间，并在程序的转换中不会改变原程序语义，满足了程序模型检测的安全性要求．     

基于状态空间模型的经济分析

探讨状态空间模型及其在经济分析与预测中的应用．状态空间模型不仅具有优良的统计性质，而且具有变量动态互动分析与预测功能．本文通过建立我国宏观经济状态空间模型并加以分析，以实证结果表明状态空间模型不失为一种较好的分析方法．     

模型与GIS集成理论初步研究

探讨了模型与地理信息系统的集成问题，指出问题的实质是对象状态数据模型、对象模拟模型和对象分析处理模型的综合表达与处理．提出了建立在元数据和元模型基础上的二层次集成方案．首先把对象状态数据模型、对象模拟模型和对象分析处理模型以规范化的元数据和元模型形式表达出来，在此基础上实现的地理信息系统、模型库管理系统和空间分析处理系统也就能提供基本的数据集成和功能集成．其次，提出了基于数据流机制的应用集成方案，满足能把应用方案数据流图化的综合性集成应用的需要．     

基于变量间依赖关系的软件可信度量模型

针对软件交互行为的动态可信度量问题,提出一种基于变量间依赖关系的动态度量模型.从输入数据对软件可信性的影响入手,利用程序静态分析和切片技术提取出关于输入信息的前向切片以及切片中各语句可赋值的变量集合,并以切片集合中的语句作为度量对象,以该语句可赋值的变量集合作为软件在该度量点处的行为预期模型.在程序动态运行过程中动态监视软件在度量点处的实际行为是否符合预期,实现可信动态度量.相应的试验结果表明,模型实现了设计目标.     

一种使用VHDL程序的硬件外演化模型

针对硬件演化中内演化过分依赖专业硬件平台的问题,提出了一种基于VHDL程序的硬件外演化模型VHDLEM。根据VHDL程序语句的不同,VHDLEM分为条件行为模型CAM和遗传程序模型GPM。CAM模型使用条件判断语句模式对电路真值表进行编码演化,得到的个体转换为条件判断形式的VHDL语句,对于输入较少的电路,CAM的演化速度快;GPM模型根据VHDL的逻辑运算语句,使用遗传程序设计的方法,演化出对应真值表的电路逻辑表达式,转换为对应的VHDL程序,对于输入较多的电路,GPM模型得到的VHDL程序较CAM更加简洁,可读性更强。     

桩基荷载传递函数扰动状态模型及应用

基于扰动状态概念，认为桩土界面单元的状态有完整状态和临界状态，受力后界面中处于这两种状态的单元服从随机分布，荷载由它们共同承担．据此建立了相应的桩基荷载传递函数模型．结合不均匀化材料的均匀化理论与概率统计方法，以桩的塑性剪切位移为分布变量，提出了模型中扰动参数的计算原理与方法．模型中，完整状态时的桩土界面单元抗剪强度采用Duncan—Chang模型计算，临界状态时的桩土界面单元承担的应力可采用传统的摩尔-库仑强度理论计算．模型具有参数较少且确定简单的特点，能反映荷载传递函数的性质，如硬化与软化，以及围压的影响．通过与实测数据的对比，验证了本文模型的准确性．最后利用建立的模型，对某工程试桩进行了分析，阐述了本文模型的工程实用价值．     

随机延时细胞神经网络的几乎必然指数稳定性

依据细胞神经网络的输出函数特征，将状态空间分解成子区域，研究了一类随机延时细胞神经网络在噪声环境下的几乎必然指数稳定性．当细胞神经网络模型的扰动项满足Lipschitz条件时，得到一些几乎必然指数稳定的代数准则．如果细胞神经网络的平衡点是子区域的内点，并且与这个平衡点相关的矩阵有一个稳定度使扰动稳定，则细胞神经网络的平衡点仍保持指数稳定的性质．所有结果只需计算网络的平衡点与矩阵的特征值．     

一种基于网络平台的工程机械监测系统

介绍一种基于网络平台的工程机械运行状态检测与故障诊断系统模型，利用网络技术实现异地工程机械状态检测与故障诊断，可实现工程机械用户与维护站或生产研家的信息交换，能够评测工程机械的运行状况与工作性能，并将评判结果形成报表通过网络传输给客户，开拓了网络技术与工程技术综合应用的新领域，系统数据库由SQLServer7建构与,种面向对象的程序软件由DELPHI5．0语言开发。     

线性离散时间系统的预测状态空间表达式

表征线性离散时间系统的参数化模型或非参数化模型可以转换为预测状态空间表达式．利用预测空间表达式可以对各种模型预测控制系统未来多步输出进行递推最佳预测，从而使其在线预测计算量大为减少．     

面向软件设计阶段的故障检测研究：模型、算法和例证

软件在国民经济和社会生活中发挥着重要作用,目前对基于故障模型的软件故障检测的研究也越来越多。分析在软件设计过程中容易发生的故障,建立故障模型;并通过分析常用的故障检测算法,总结算法存在的不足,同时提出一种基于状态变迁缩减的启发式搜索算法。此算法只需要检测系统中的部分状态变迁,就可以提高对系统中故障的检测能力。实例表明:该算法对建立的扩展有限状态机故障模型是有效的。     

基于有界模型检测的门级软件自测试方法

提出了基于有界模型检测的门级软件自测试方法.将处理器中的模块简化成约束模块,缓解状态爆炸问题.将难测故障的触发条件逐个转化成性质并且采用有界模型检测技术,搜索触发这些性质的违例.最后,将违例映射成测试指令序列,并为测试指令序列添加观测指令序列,构成自测试程序.实验结果表明:该方法在不引起状态爆炸问题的情况下,有效地测试控制器中难以测试的故障,提高了在线测试的测试质量.     

线性混合系统的一种验证方法

混合系统是指嵌入于物理环境中的数字实时系统．由于计算机技术的快速发展,混合系统在各行各业中都得到广泛应用,但是由于混合系统涉及到连续时间,因此其验证问题始终没有得到完善的解决．近年来,人们普遍采用模型检验方法对混合系统进行验证．由于线性混合系统在实际应用中可以表示大多数的嵌入式实时系统,因此我们着重研究这类混合系统的验证算法．本文首先介绍了混合系统的模型—混合自动机,然后提出了一种针对线性混合系统的基于区域的先划分再遍历的半确定性验证方法．经实例检验,该方法能够有效地验证线性混合系统．最后将本文的方法同有关的其它算法进行了比较     

一种基于CPN的协议测试序列生成方法

针对状态空间规模较大的协议,提出了一种基于着色Petri网CPN(ｃolored ｐetri ｎet)、面向属性的协议一致性测试序列生成方法。 首先, 构建被测协议规范的CPN模型, 即协议模型, 并将被测协议的若干功能属性采用CPN进行形式描述, 形成属性模型。 提出了属性模型到协议模型的状态投影算法、模型状态空间的路径匹配算法和搜索算法, 基于这些算法给出了一种完整的基于属性的测试序列生成方法。 该方法不但可以有效避免协议规模庞大所导致的状态爆炸问题, 而且还对测试中的PCO库所进行了特殊标识, 完成测试序列中可观察元素的自动提取处理, 使得处理后的测试序列可直接用于协议实际测试过程。 为有效验证所提测试序列生成方法的可行性, 开发了一套实现该方法的软件, 并应用于HMIPv6协议的实际测试过程中。实践表明, 这套软件可以对较为复杂的协议一致性测试过程提供强有力的支持。     

基于并行环境的模型检查技术研究与实现

针对实时系统模型检查中的突出问题：状态组合爆炸,提出一种基于并行环境的实时系统模型检查技术,用邻接表存储时钟带,用C＋＋和MPI设计并实现了一个并行实时系统模型检查器———PRAModelChecker,选择一个典型的实例对PRAModelChecker的性能进行分析.实验表明,随着系统复杂性的增加,不但能提高工作效率,而且能处理的系统规模可伸缩,从而为从根本上解决状态组合爆炸问题提供了一种新的途径.     

基于混成自动机的CPS行为建模与属性验证

系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上,提出了一种CPS行为建模与属性验证方法。该方法首先基于混成自动机对CPS的行为进行建模,然后将此模型转换为混合程序模型,最后在定理证明器KeYmaera中对HP模型的属性进行形式化验证。文中论述了行为模型描述语言的结构,建立了混成自动机模型与HP模型之间的转换规则,分析了模型转换的一致性。应用实例表明:该方法既能简单直观地描述CPS动态行为,又能对CPS的属性进行严格的形式化验证,且有效避免了形式化验证中的状态空间爆炸问题。     

结合多尺度特征和多维注意力的人脸风格转换

针对StarGANv2模型生成的人脸图像存在风格重建效果不佳、人脸纹理不够自然等现象,该文提出结合多尺度特征和多维注意力的人脸风格转换模型.1)将多尺度特征融合模块PSConv嵌入StarGANv2生成器内,提高了模型对图像特征的提取能力;2)提出了多维注意力模块MDConv,并将该模块嵌入StarGANv2判别器内,从而提高了模型对真假人脸图像的判别能力.与StarGANv2方法在CelebA-HQ数据集上进行对比实验的结果表明：该方法生成的人脸图像风格更美观,纹理细节更自然,学习感知图像相似度(LPIPS)的值也得到了提升.     

一种基于UPPAAL的智能合约属性形式化验证方法

针对智能合约的属性验证问题,该文提出了一种基于UPPAAL的智能合约属性形式化验证方法.首先定义了Solidity基本语句的操作语义及其到时间自动机的转换,将智能合约转换成时间自动机网络模型;然后定义并描述智能合约常见的安全性和活性,再使用模型检测工具UPPAAL验证智能合约的属性;最后对购物合约进行了建模与验证,验证了该方法的有效性.     

蚂蚁算法在概念设计方案求解中的应用

通过分析概念设计方案求解问题与旅行商问题的相似性，将方案求解问题转化为组合优化的最优路径问题，建立了基于动态规划的解空间模型和基于最长路径的优化模型，利用蚁群系统内在的正反馈寻优机制，将求解旅行商问题的基本蚂蚁算法应用于方案求解的组合优化过程，结合遗传算法的交叉变异操作，提出一种基于改进蚂蚁算法的求解方法，从而快速有效地获得了最优方案解，最后，以压力机的概念设计为例验证了该方法，研究表明，该方法是合理可行的，它可以使方案求解的人工寻优过程实现算法化，并具有较好的可操作性，从而为解决方案优化的组合爆炸问题提供了一种新的思路。     

一种编译指导的实时动态电压调节低功耗算法

提出了一种编译指导的实时动态电压调节低功耗算法.算法在编译器的帮助下,在条件语句,循环语句等影响程序实际执行时间的控制语句结构中设置电压调节点,插入电压调节代码,从而最大限度地利用了程序运行时的空闲时间,达到了降低系统功耗的效果.在RTLPower实时低功耗系统上对算法进行了实验,实验结果表明该算法可以减少50%的能量消耗.