时间自动机与信号自动机的互模拟算法

基于时间自动机的验证工具已被广泛应用于实时系统模型验证。信号自动机为一类实时系统建立了比时间自动机更适合的模型,但是它还不能用于实际的实时系统模型验证,因为没有验证算法可用。把信号自动机验证问题归约到了时间自动机验证问题：证明了两种自动机具有相同的识别语言能力,证明了二者具有双向模拟关系,并在此基础上提出了线性的互模拟算法。把互模拟算法和已有的时间自动机验证算法结合起来,就得到了信号自动机的验证算法,从而解决了对信号自动机模型的验证问题。     

一种基于时间自动机网络的实时系统形式化验证方法

介绍了时间自动机形式模型,在此基础上给出了时间自动机网络的形式语法和语义,然后给出一种基于时间自动机网络的实时系统形式化验证方法,并采用基于时间自动机网络的模型检测工具UPPAAL对一个经典的实时系统实例进行了验证．     

一种时间自动机时钟离散化算法

稠密时间自动机被广泛应用于实时系统自动验证.然而其在补操作下不封闭,因而导致多种线性实时性质不可验证.离散时间自动机虽不存在此问题,但该模型表达能力偏弱.因此,提出了一种时间自动机时钟离散化算法,结合时钟物理约束因素,证明了新方法可有效解决上述问题.     

扩展线性时段不变式的模型检验研究进展

扩展线性时段不变式是时段演算中的一类重要公式.时段演算是周巢尘院士于20世纪90年代提出的一种用于嵌入式实时软件设计的演算系统,它开创性地将积分概念引入计算机实时软件的分析中,从而能够描述处理连续时间区间性质,是国际上公认的描述和分析实时系统的主流方法之一.由于时段演算内容丰富并且相关的综述和专著已出版,文章旨在对扩展线性时段不变式这一时段演算子集的模型检验问题的研究情况进行论述:①介绍时段演算、线性不变式及其扩展;②分别论述线性时段不变式以及扩展线性时段不变式的模型检验研究情况,其中重点介绍扩展的线性时段不变式,在离散时间语义和连续时间语义下的近期验证成果.     

广义线性模型的诊断与实例分析

研究了广义线性模型的诊断，将线性回归模型的诊断方法推广运用到广义线性模型，证明了均值漂移模型与数据删除模型的等价性，研究了判断异常点的Score检验统计量．最后通过实例建模，验证了本文给出的诊断方法的有效性．     

基于CheckMate的混合系统建模和验证

形式验证是混合系统中的重要研究方向,Checkmate是基于MATLAB/Simulink和Stateflow工具箱开发的一种混合系统建模、仿真和形式验证工具。文章首先介绍了混合系统形式验证的概念和验证过程,从用户的角度介绍了CheckMate的每个自定义模块的设置及其功能原理,通过一个三维线性混合系统的例子,说明了使用CheckMate进行建模、仿真以及验证的方法,最后指出了CheckMate验证工具的局限性。     

交直流混合电力系统的无功优化研究

本文对交直流混合电力系统的无功优化问题进行了研究．建立了交直流混合电力系统的无功优化数学模型,该模型的目标函数为交流网络的有功损耗和直流网络的有功损耗之和,优化控制变量考虑到混合电力系统中交流部分以及直流的影响．针对交直流混合系统的特点,提出了适合求解混合系统无功优化问题的实用算法．     

检验实时系统的有序时段性质

模型检验是一种被广泛应用于对设计或系统正确性进行自动验证的技术。实时系统的性质包括瞬间性质和时段性质，显然后的检验要比前复杂得多。介绍了一类新的时段性质——有序时段性质，并检验了时间正则表达式的有序时段性质，最后分析了算法的复杂度，和相关工作进行了比较，并探讨了今后的工作方向。     

竞争失效产品加速寿命试验的广义线性模型分析

本文利用广义线性模型方法研究了竞争失效产品恒定应力加速寿命试验的统计分析，其联系函数由产品各失效机理的加速方程组成，这样利用广义线性模型软件可得到参数估计，在计算上简便可行，同时我们还得到加速方程系数ｂ１．．．ｂｍ相等的检验方法。     

基于量子行为的模拟移动床的操作优化

模拟移动床是一种能实现连续分离的装置,由于模拟移动床模型复杂,性能指标众多,因此需要智能算法对模拟移动床的性能指标进行优化。本文运用遗传算法、粒子群算法对模拟移动床线性吸附等温线下的性能指标进行单目标优化,并利用加入量子行为的粒子群和遗传算法作比较,证明了量子理论在解决模拟移动床优化问题的优越性,然后运用NSGAII算法、MOPSO算法对模拟移动床线性吸附等温线下的性能指标进行多目标优化和对比实验,仿真结果验证了所用方法的有效性。     

基于模型检测的实时模型诊断方法

提出一种基于模型检测的实时模型诊断方法. 利用 模型检测算法对大状态空间系统验证的高效性, 使诊断系统能够更快地进行模型诊断, 并对这种方法进行了系统实现, 结果表明, 此方法可行、 有效.     

基于切换表面状态划分的倒立摆模型验证

针对仿真对不存在或难以寻找的问题,利用商迁移系统,给出了混合系统的验证过程。结合倒立摆模型给出的只对状态空间切换表面进行离散化的空间划分方法,相对于常规验证所采用的离散整个连续状态空间的方法,降低了系统分析的维数。提出将阈值切换切分为两类,明确了切换面的划分方式。     

混合动态系统的模糊接口设计

利用模糊逻辑控制的思想,给出了混合系统的模糊接口设计.该接口通过其内部参数的学习把连续状态空间划分成多个子空间,使受控对象的非线性系统在每个子空间内可由一基于模糊逻辑的线性模型逼近,从而简化了对象模型和设计任务.当连续状态穿越空间边界时,则由上层离散事件控制器进行模式切换,从而使系统以稳定安全的方式运行.     

一种改进的实时系统可达性分析算法

首先简介了时间自动机、时钟区域、区域等价、时钟带的概念.利用时钟带,可以将时间自动机的无穷状态空间转化为有穷.实时系统的绝大多数安全性和部分活性可以通过可达性分析算法来验证.然而,当系统时钟个数较多时,用DBM存储时钟带,会造成内存空间的很大耗费.该文提出了用邻接表存储时钟带,给出了改进的算法,并对算法的空间复杂度作了分析.实验表明,当时钟个数大于5时能节约很大的内存空间,从而在一定程度上缓解了状态爆炸.     

一类混合系统不变集LMI方法求解

本文主要探讨了混合系统和不变集的研究,介绍了理论产生的背景,阐述了混合系统的概念和混合自动机建模, 由LaSalle提出的不变集理论在文中首先作了介绍并给出了主要的计算方法迭代法;在混合系统中,提出了通过构造李雅谱诺夫函数利用线性矩阵不等式的方法求得不变集的存在,同时不变集的范围也可以进一步求得;接着一个混合系统数值仿真例子证明了该方法的可行性与有效性,最后介绍了讨论混合系统不变集的应用和下一步的工作。     

马尔科夫跳变系统的H∞-自适应变结构控制

研究了一类带有一般不确定转移速率的非线性广义时滞马尔科夫跳变系统的H_∞-自适应变结构控制问题.首先,针对系统中的非线性未知参数设计由线性控制器和自适应控制器组成的混合控制器,构建Lyapunov泛函,使得系统的轨迹趋近于状态空间曲面且闭环系统随机容许,满足H_∞性能γ.进而考虑一般不确定转移速率矩阵的特性,构造严格线性矩阵不等式,使结论更具一般性.最后,通过数值算例及图像仿真验证了这类控制方法的有效性和可行性.     

铁路系统的模型检查和参数分析

研究铁路系统的自动验证技术，建立火车和控制器的混合自动机模型，用时态逻辑ＩＣＴＬ描述铁路系统的性质规范，使用模型检查技术自动验证铁路系统，并且对铁路系统的一些参数进行分析。     

Hybrid Dynamic Modeling and Control of Molten Carbonate Fuel Cell Stack Shutdown

A hybrid automaton modeling approach that incorporates state space partitioning, phase dynamic modeling and control law synthesis by control strategy is utilized to develop a hybrid automaton model of molten carbonate fuel cell （MCFC） stack shutdown. The shutdown operation is divided into several phases and their boundaries are decided according to a control strategy, which is a set of specifications about the dynamics of MCFC stack during shutdown. According to the control strategy, the specification of increasing stack temperature is satisfied in a phase that can be modeled accurately. The model for phase that has complex dynamic is approximated. The duration of this kind of phase is decreased to minimize the error caused by model approximation.     

无限维混杂系统及其稳定性

该文基于半群理论对无限维的系统进行了建模,给出了用半群理论的无限维的混杂系统的模型,在此模型的基础上给出了其渐进稳定和一致有界的定义,并根据多Lyapunov方法等手段给出了几个无限维混杂系统在任意切换的情况下渐进稳定的条件。针对于无限维的线性切换系统,给出了具有有限个子系统的情况下的公共Lyapunov函数存在的条件,扩展了已有文献中的成果,最后还基于循环算子的定义和性质给出了一个等价的定理。     

岩体中无限区域软弱夹层的模拟

提出平面四结点映射夹层无限元模型及相应算式，在半无限区域的岩土工程中，用此单元与夹层有限单元耦合系统模拟无限区域的软弱夹层，节省了大量的数据准备工作量和机时，了计算精度。