中尺度暴雨模式MRM1简介及预报效果检验

介绍了近年来我们所研制的中尺度暴雨模式MRM1的基本情况及特点，以及对1998年，1999年和2001年6月、7月的降水集中时段进行的逐日降水预报试验及效果检验，并和美国著名中尺度模式MM5进行了同一时段降水预报检验的比较。结果表明，它是目前国内较好的中尺度暴雨预报模式，在暴雨预报方面较MM5也有一定的优越性。     

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

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

中国股票市场的日内波动特征研究

采用沪深300指数的日内数据，运用方差分析并进行方差检验的方法，对各个时点间隔24小时的收益率波动情况进行分析，发现在交易期间收益率方差呈现“W”型变化，且交易时段的收益波动要大于非交易时段的收益波动。     

居民区电动汽车有序充放电控制策略

针对目前居民区配电装置额定容量不能满足大量电动汽车充电需求的问题,提出了一种考虑充放电接入退出随机性的电动汽车有序充放电控制策略.该策略以峰谷分时电价为背景,使电动汽车在负荷高峰时段向电网馈电、在负荷低谷时段充电以实现削峰填谷,并在充放电起始和结束时刻进行一定的随机性处理,使得负荷曲线更加平滑,避免总负荷瞬时突变.最后通过时序仿真验证了有序充放电控制策略的有效性.     

基于时段自动划分的交叉口混合控制方法

针对交通控制中时段划分的主观性,提出了基于有序聚类的交叉口时段自动划分方法,根据Fisher最优分割原理,实现了时段的科学有效的划分;利用时段划分结果,采用混合控制策略对交叉口进行控制,实验表明与感应控制和定时控制相比,该方法可有效改善道路的交通状况.     

中尺度暴雨模式MRM 1作者简介及预报效果检验

介绍了近年来我们所研制的中尺度暴雨模式MRM1的基本情况及特点,以及对1998年,1999年和2001年6月、7月的降水集中时段进行的逐日降水预报试验及效果检验,并和美国著名中尺度模式MM5进行了同一时段降水预报检验的比较.结果表明,它是目前国内较好的中尺度暴雨预报模式,在暴雨预报方面较MM5也有一定优越性.     

磁场对多铁性材料 CdCr2 S4介电性质的影响

多铁性材料在磁相变温度附近的介电异常归因于系统中铁磁有序和弛豫铁电性的共存。本文基于Heisen-berg模型对铁磁子系统进行分析,使用最近邻自旋对关联表征磁子系统的磁有序程度。磁性质通过磁电耦合效应修正磁性离子因非中心位移而形成的极化簇的取向激活能,实现对介电性质的影响。外加磁场通过提高系统的磁有序程度而使得介电异常更为显著,磁相变温度附近的磁电容效应是磁场对介电性质影响的最好检验。     

闭正则模糊拟阵单点收缩子拟阵的基有序性质

该文研究了模糊拟阵的单点收缩子拟阵的基有序性质;在闭正则模糊拟阵的单点延拓的基有序基础上,研究了闭正则模糊拟阵单点收缩子拟阵的基有序的若干性质,得到了闭正则模糊拟阵的单点收缩子拟阵的基有序性质是保持的,并举例说明了闭正则模糊拟阵的单点收缩子拟阵的基有序性质.     

网络协议的形式化分析与设计

随着形式化方法和技术的日趋完善,网络协议的开发已逐步从非形式化描述、手工方法实现过渡到已形式化描述技术为基础,渗透到网络协议分析、综合、测试等各环节的软件工程方法。本文从网络协议的基本要素、协议的形式化模型介绍了网络协议,并从协议的性质描述、不变性分析、可达性分析、基于有序二叉判决图的符号模型检验对网络协议进行了形式化设计与验证,最后进行了测试。     

基于有序树的广义表运算算法设计

通过分析与研究广义表与有序树之间的关系和性质,并在相关文献对广义表的研究基础上,提出了基于有序树的广义表表头、表尾、长度和深度的定义,并根据有序树的二叉链表表示法对以上定义进行算法设计.     

软件体系结构动态特征建模与验证

针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词/变迁(Pr/T)网为软件体系结构动态行为建模,并提出了基于线性时序逻辑的软件体系结构动态行为模型验证方法.首先根据体系结构层次模型扩展Pr/T网建立体系结构动态行为模型(DFM)并构造DFM的可达图,然后使用基于自动机理论的方法来验证模型的时态逻辑性质,最后通过对一个电子商务系统实例的并发控制机制建模和模型检测,验证了该方法的有效性.所提方法结合了Pr/T网和线性时序逻辑的优点,为进一步开展软件体系结构动态行为的分析、验证奠定了基础.     

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

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

基于二级倒立摆实验装置模糊控制

引入模糊控制改善原有的线性控制算法,对二级倒立摆实验装置系统进行了二次开发。将经验和基于系统仿真结果相结合,制定出了简单适用的规则库。该实验系统的实例仿真及调试结果表明,系统具有良好的稳定性,在抑制外部扰动和实时控制性方面,本方法优于经典的状态反馈最优控制。     

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

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

一种扩展型实时多数据库系统实现框架

实时多数据库系统提供了一个实时数据集成管理平台,它不仅可以处理传统数据库中的持久性数据,而且可以处理实时系统中的即时数据.首先简介了实时多数据库系统的特征,给出一种扩展型实时多数据库系统RT-Panorama的体系结构,和基于XML的实时数据模型XRTDM作为RT-Panorama的公共数据模型,针对实时多数据库系统的时限要求给出了RT-Panorama中的实时消息处理机制.     

Model Checking over Paraconsistent Temporal Logic

Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies （inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed）. In this paper, we propose the use of a guasi-classical temporal logic （QCTL） for supporting the verification of temporal properties of such systems even where the consistent model is not available. Our models are paraKripke structures （ extended standard Kripke structures）, in which both a formula and its negation are satisfied in a same state, and properties to be verified are expressed by QCTL with paraKripke structures semantics. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.     

基于灰色模型的广义预测控制直接算法

基于灰色模型GM（1,2）,采用两个辨识器分别辨识被控对象和闭环系统的参数,从而得到了控制器的参数,给出了一种广义预测控制的直接算法.由于此方法将被控对象视为灰色系统,需辨识的参数较基于CARIMA或CARMA模型的广义预测控制直接算法大大减少,实时性进一步提高.仿真结果表明,该方法是有效可行的.     

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

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

基于核和灰度的区间灰数行列式的若干性质

为了简化区间灰数行列式的运算,完善区间灰数的运算和灰数代数系统的理论基础,利用区间灰数的简化形式探讨区间灰数行列式的性质,得到了基于核和灰度的区间灰数行列式的若干性质,简化了区间灰数行列式的运算,为进一步探讨区间灰数矩阵及区间灰数线性方程组奠定了基础.     

一种广义预测控制直接算法

基于灰色模型GM（1，2）采用两个辨识器分别辨识被控对象和闭环系统的参数，从而得到了控制器的参数，给出了一种广义预测控制的直接算法。由于此方法将被控对象视为灰色系统，需辨识的参数较基于CARIMA或CARMA模型的广义预测控制直接算法大大减少，实时性进一步提高。仿真结果表明，该方法是有效可行的。