时间自动机与自动验证

给出时间自动机的基本概念，描述了区域自动机的构造方法，并且实现了区域自动机的构造算法，简述了通过时间自动机进行自动验证的过程，最后分析了区域自动机构算法的时间复杂度。     

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

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

基于细胞自动机的信号控制交叉口交通流模拟

应用细胞自动机方法对信号控制交叉口的动态交通流进行建模和模拟,可以使比较复杂的交通状态模拟用相对简单的计算来实现。介绍了几种用于交通流模拟的细胞自动机模型及其研究进展,在上基础上,给出了一种新的细胞自动机模型来描述车辆在交叉口的转移状态,讨论了交通拥挤和延误的二维演变,并用这一方法模拟了不同规则下的车道变换问题,通过比较模拟结果和原始输入方案可以优化信号配时。     

基于时间自动机的UML模型转换与验证研究

针对无法对UML模型进行形式化验证的问题,提出在元模型层将UML模型转换为时间自动机模型并进行验证的方法.形式化UML状态机的结构,抽象出UML和时间自动机的元模型,利用模型转换语言ATL对UML元模型和时间自动机元模型构造映射规则,实现UML模型到时间自动机模型的转换,在模型验证工具Uppaal中对转换结果进行形式化验证.最后进行实例研究,结果表明了此方法的有效性和先进性.     

时间自动机与自动验证

给出时间自动机的基本概念,描述了区域自动机的构造方法,并且实现了区域自动机的构造算法.简述了通过时间自动机进行自动验证的过程,最后分析了区域自动机构造算法的时间复杂度.     

时间自动机的事务级形式验证

提出了一种形式方法用于验证TLM-2.0的设计方案.该方法中TLM-2.0设计方案将被转换成定时自动机形式模型.定义若干种属性,验证将根据这些属性执行,并引入一种模拟事务级设计方案差错的故障模型来评估这些属性.然后这些属性通过使用形式UPPAAL验证工具在系统的定时自动机表示上针对这些故障被验证.最后通过一个实例研究说明该方法的有效性.     

基于细胞自动机理论的交通流模拟模型

以细胞自动机理论为基础,结合我国城市道路情况及交通流特性,把车辆在路段上运动的变化规律表述为细胞自动机的演变规则,建立了基于细胞自动机理论的交通流模型,标定了细胞长度和最大速度等参数,继而提出了反映车辆在路段上自由驶、跟驰行驶和减速行驶等交通行为的细胞自动机规则,并对各种规则进行了详细说明。     

基于概率时间自动机的模型检测反例表示研究

近年来,概率系统在实际中应用越来越广泛,其中模型检测基于概率系统的反例生成问题,已引起人们的广泛关注,现有的工作主要围绕模型检测Markov链反例生成展开.概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展,针对模型检测PTA的反例表示问题,首先将PTA的语义表示为Markov决策过程(MDP),通过策略解决MDP不确定性,将MDP转换为离散时间Markov链(DTMC);然后将DTMC转换为带权有向图,则PTA中最小反例问题转化为带权有向图中最短路径问题;最后采用正则表达式表示求得的反例.     

对时间输入/输出自动机一致性测试的改进

Jan.S等提出了对时间输入／输出自动机（TIOA）模型进行黑盒一致性测试的算法。针对其生成的测试序列数量太大这一问题，提出用可最小化的时间自动机（MTA）模型来描述稠密的实际系统，并用递归算法实现了对测试序列的首部即转换覆盖P的构造。由分析得出结论：使用MTA模型可使上述测试算法生成的测试序列的数量大大减少，从而在不影响其完全性的情况下使该算法更具实用性。     

模拟生命系统的细胞自动机建模方法

本文介绍了细胞自动机的基本概念并给出了建模方法。作为一个应用实例，文中建立了一个细胞自动机模型，它能模拟在同质环境中不同的初始配置和竞争关系对种群分布格局的影响。通过模拟，我们发现模拟结果支持假说－“初始配置对种群最后的分布格局具有重要的影响”。     

元胞自动机中斑图复制的识别算法

给出了元胞自动机中斑图复制识别的一种算法。通过定义每个元胞的特征数,将两个斑图统一放入一个区域内比较它们的特征数,从而判定是否出现复制现象。数值例子表明,该算法是有效的。     

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

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

禁止字方法在元胞自动机中的一个应用

给出了使用禁止字理论、计算机搜索和符号动力学研究初等元胞自动机演化语言的一种方法，并且使用该方法得到了27号初等元胞自动机演化语言在数学上的精确描述．     

基于元胞自动机模型的内陆河三角洲堆积体演化过程

通过建立二维元胞自动机模型,对山区河流直接进入开阔湖区后的内陆河三角洲堆积体演化过程进行研究。分析三角洲堆积体的发展过程和堆积体表面冲积河槽形态演变的规律。总结得出整体规律:先纵向推进,再垂向淤积抬升,最后横向展宽;纵向推进速率随着模拟步数的增加而减小;垂向逐渐淤积抬升;横向展宽速率随着模拟步数的增加而逐渐减小;堆积体表面的河槽形态演化分为顺直、分汊和微弯河槽3个阶段。模拟结果与已有类似物理模型试验结果基本吻合,表明元胞自动机模型可以用于模拟三角洲演化的过程。     

基于元胞自动机的无信号人行横道处人车干扰机理研究

为了更准确地模拟行人与机动车的干扰机理,提出了基于元胞自动机的人车干扰模型。模型主要由机动车避让模型、行人过街决策模型以及运动模型组成。该模型不仅考虑了行人的主动性决策行为,还考虑了机动车的主动避让行为,重点分析了人行横道等候区域处,行人对机动车避让行为的影响。仿真结果显示,机动车旅行时间随着机动车限制速度的提高而减小,逐渐趋于平缓;机动车的饱和流量随着行人到达率的增加而降低;机动车的延误随着等候区人数的增加由线性增加逐步趋于平缓。     

标准元胞自动机模型的缺陷及拓展研究

具备时空计算特征的元胞自动机模型（CA）与GIS集成将极大促进GIS对地理过程的模拟能力。标准元胞自动机在元胞形态、邻居规则等方面的定义存在极大限制，制约了元胞自动机对真实世界的模拟和应用能力。论文充分研究了空间模型与元胞邻居描述的关系，发现元胞邻居在空间关系上存在拓扑邻接、空间邻近和复杂相离三种关系，传统思路的模型扩展很难完全解决CA的局限性，尤其是复杂相离关系。为此，论文在面向对象的思想基础上提出了基于地理实体的元胞自动机概念模型。     

Sub-classes and evolution stability of Wolfram''s classesin the total-rule cellular automata

In this paper, we propose a concept of sub-classes and its evolution stability for the Wolfram's classes. Firstly, we obtain the sub-classes of the Wolfram's class IV, gene-piece of these sub-classes and their existing circumstance. Secondly, we introduce a new concept, the evolution stability, for the Wolfram's classes and sub-classes of Wolfram's class IV. Lastly, we find that Wolfram's classes I, II, and III have the evolution stability, but sub-classes of the Wolfram's class IV have not the evolution stability for the total rule cellular automata.     

移频信号解调算法研究与DSP实现

随着我国高速铁路的快速发展,快速准确的检测列车自动控制系统中轨道电路移频信号参数成为了列车安全运行的重要保证.针对现有轨道电路移频信号检测算法在检测精度和检测时间上的局限,以及传统测试仪在智能化上的不足,对移频信号的频谱特点进行了分析研究,基于频谱特点利用欠采样技术和汉宁窗频谱重心校正算法对移频信号参数进行了解算,并基于DSP搭建了实验平台对算法进行了移植和实测验证.实验结果表明,该算法能够快速准确地自动检测出移频信号的各项主要参数.     

基于地理栅格数据和元胞自动机的城市数字进化仿真模拟

建立了基于栅格地理数据和细胞自动机的城市数字进化仿真的演化模型。该模型能根据一段时期内的地理信息数据,挖掘和发现城市的发展变化对地理信息数据的周期规律,并且能够对城市的发展变化进行模拟,最后通过仿真实验验证了该模型的有效性。     

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

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