许丹[1]2007年在《基于时间自动机的实时系统形式化建模与验证》文中指出实时系统是一种带有时间约束的计算机系统,这些系统的许多动作的完成是与时间相关的,即要满足一定的时间限制。为了确保实时系统的正确性和可靠性,需要对其进行严格的分析和验证。实时系统的验证不仅要求逻辑上是正确的,而且要求时间上也是正确的。时间自动机是使用最为广泛的实时系统形式化建模工具。本文在R.Alur等人提出的时间自动机的基础上深入研究了实时系统建模与验证理论及其实际应用。本文给出时间自动机的形式化定义,研究了基于时间自动机的实时系统建模方法,并给出了时间自动机模型的优化方法。最后对两个实时系统进行分析,利用时间自动机对它们建模。实时系统验证主要验证的问题分为安全性验证问题和活性验证问题,安全性验证问题可归结为时间自动机的可达性分析,由于模型检测方法在对系统验证时存在状态空间爆炸问题,因此,系统需要一种能较好解决该问题的自动规范验证技术。为了解决区域自动机构建过程中出现的状态空间爆炸问题,我们还引用了启发式验证方法。本文主要研究了基于历史等价和转换互模拟的最小化方法。经过最小化后,大大缓解了状态空间爆炸问题。UPPAAL是一种以时间自动机作为行为模型的模型验证工具,它在实时系统的自动验证中占据重要位置。在对UPPAAL的基本结构和工作原理分析之后,我们发现它采用的限制技术和快速验证技术可以避免构建状态空间中的不可达状态,能在一定程度上解决状态空间爆炸问题。最后利用UPPAAL对已建立的两个实时系统的时间自动机模型进行性能验证,证明了它们的正确性和安全性。
康仁伟[2]2013年在《基于时间自动机的CTCS-3级列控系统建模方法与验证研究》文中进行了进一步梳理CTCS-3级列控系统的实时性依据技术规范而实现。如果技术规范存在缺陷,则会严重危及行车安全或影响行车效率。因此,有必要对列控系统的实时性进行分析研究,以验证技术规范的正确性。目前,验证系统实时性的途径有仿真、测试、形式化方法叁种。仿真和测试存在固有的缺陷,形式化方法可以最大限度地分析验证系统。通过比较多种验证系统实时性的形式化方法得出：时间自动机理论更为适合验证CTCS-3级列控系统的实时性。本文提出一种基于时间自动机的列控系统建模与验证方法。科学地阐述时间自动机模型与列控系统的一致性、所建模型的正确性、模型验证结果的可信性等问题,创造性地提出对列控系统进行VV&A分析的原则和过程,建立了基于时间自动机的列控系统建模与验证框架,并说明了该建模与验证方法对CTCS-3级列控系统各个运营场景的普遍通用性。其建模与验证的一般流程为：用时间自动机语言规约列控系统的行为和动作,得出列控系统的时间自动机模型,然后用UPPAAL验证工具对系统模型所反映的特性进行验证。以CTCS-3级列控系统临时限速和等级转换运营场景为例,说明了该建模与验证方法的有效性。利用时间自动机理论,分别建立临时限速工作流程、等级转换过程的时间自动机网络模型。同时,应用UPPAAL验证工具对临时限速系统、等级转换过程的安全性和受限活性进行仿真分析。找到了临时限速技术规范中不能达到实时性要求的时间参数设置,并给出了修正值。此外,等级转换模型成功验证了等级转换过程的安全性。验证结果表明：该建模与验证方法可有效研究CTCS-3级列控系统临时限速和等级转换的实时性。
贺伟[3]2017年在《基于时间自动机的行车许可的建模与验证》文中研究表明CTCS-3级列车运行控制系统是我国引进、吸收然后再创新的列控系统,它极大的提高了高速列车的运行效率和安全性。RBC是CTCS-3级列控系统中的核心设备,由它生成行车许可命令能够保障列车顺畅运行。因此,分析RBC生成行车许可的流程并利用形式化方法建模和验证系统规范的正确性是十分必要的,本文采用时间自动机理论对CTCS-3级列控系统的叁种场景下行车许可生成进行建模仿真和验证。在验证系统的实时性时,形式化方法是一种保障正确性和可靠性的重要途径。RBC是一种典型的实时系统,而时间自动机是专门为了研究实时系统的,它能够较完整的描述实时系统的时间特性,因此,本文选用时间自动机理论对RBC系统生成行车许可建模。模型的验证需要利用合适的实时系统模型验证工具,通过对比本文运用实时系统验证工具UPPAAL进行验证。论文依据《CTCS-3级列控系统总体技术方案》和《无线闭塞中心(RBC)技术规范》详细的分析了CTCS-3级列控系统行车许可生成、等级转换和RBC切换的流程,各设备之间的通信连接和信息交互过程。同时需要提取需要验证的功能属性和时间属性。在建模过程中,首先是确定建模对象,例如各种硬件设备;然后,根据研究对象之间的联系,提取抽象对象的行为和动作并映射为形式化语言;最后,确定模型的状态跳转路径和约束条件,得到相应的时间自动机模型。利用UPPAAL工具中对系统模型进行模拟,通过随机得到的仿真序列观察研究对象的信息通信和状态变化。同时,应用工具中的验证器验证了研究对象的功能属性和受限活性。论文完成了RBC生成行车许可的建模与验证。研究结果表明所建模型满足技术规范的功能属性和安全性要求。
赵丽芳[4]2008年在《基于UPPAAL和UML的实时系统形式化分析与应用》文中认为计算机的应用模式在经历了主机模式和个人机模式后,目前正向最适合人类使用的普适计算模式发展。在普适计算模式下,实时系统将会渗透到人们生活的方方面面,为提高人们的生活质量发挥重要的作用。在这种情况下,实时系统的质量和开发效率往往会对一个产品的成功起着决定性的影响。为了保障实时系统的实时性、安全性和可靠性等,本文在深入研究了时间自动机、UPPAAL、UML的理论基础上,采用时间自动机与UML相结合的建模方法,使用UPPAAL对所建模型进行分析与验证,并结合两个实例说明了本方法。采用形式化方法对实时系统进行分析和验证是提高其安全性、可靠性的一条重要途径。目前时间自动机是用于实时系统建模的重要形式化工具,它刻画了实时系统与时间有关的行为特征,反映了实时系统控制行为的可视转向。UML顺序图着重体现对象间动态的交互关系,而且具有良好的易理解性。但是UML顺序图用来对实时系统建模和验证还存在时间描述方面的不足,因此本文研究了利用UML的扩展机制对UML顺序图进行扩展的方法,扩展后的UML顺序图不但能够很好地保持原来的易理解性,而且能够精确地描述实时系统的时间需求。使用扩展后UML顺序图对实时系统建模,结合UML顺序图与时间自动机的形式化语义,将顺序图转化为时间自动机,然后采用模型检测工具UPPAAL对其进行形式化的分析与验证,最后结合咖啡机控制系统与交通灯控制系统实例,进一步说明本文所给方法在实时系统中的应用。
姬莉霞[5]2004年在《基于时间自动机的实时系统规范验证研究》文中进行了进一步梳理实时系统不仅要求逻辑上是正确的，而且要求时间上也是正确的，这类系统在设计阶段需要进行严格的分析和验证。时间自动机是使用最为广泛的对实时系统进行规范验证的形式化方法之一。 实时系统验证主要分为安全性验证和活性验证，系统的活性可以通过位置的不变式和转移的约束条件保证，验证也比较容易，本文对此不作过多讨论。安全性验证问题可归结为时间自动机的可达性分析，基于状态空间搜索的方法主要不足在于状态空间的大小随着过程数目的增加呈指数级递增，这就导致了状态空间爆炸问题。为了解决这个问题，我们必须构造时间自动机状态空间的有穷表示。 本文主要研究了Alur提出的域自动机方法、带自动机方法以及Inhye Kang等提出的状态空间最小化方法，并在此基础上提出了时间段转换系统以及对状态空间的极小化方法。该方法用位置和进入位置的最大最小时钟值集合来表示状态而得到时间段转换系统，同时通过转换分析保留有效转换来简化这个转换系统。对简化后的系统，使用转换互模拟进行最小化。文中对该方法进行了可行性分析，通过与其它方法进行比较阐述了该方法的优点和不足，并建立了铁路交叉口控制门系统的最小化过程。 在规范验证应用方面，本文研究了两种典型实时系统——道岔自动控制系统和自动筛选器系统。通过对系统进行分析和规范，给出了系统的时间自动机模型，并使用UPPAAL对模型进行验证，证明了系统的安全性、有效性和可控性。
王静[6]2005年在《基于时间自动机的模型验证理论及应用研究》文中研究表明实时系统是一类重要的计算机应用系统,它经常被使用在对安全性要求极高的操作环境中,因此确保此类系统的正确性至关重要,并且需要我们使用形式化的方法对实时系统进行规范验证。 本文在R. Alur等人提出的时间自动机的基础上深入研究了系统模型验证理论及其实际应用。我们通过判定实时系统以及它的规范说明所对应的时间正则语言的交集是否为空对实时系统进行规范验证,比较常用的验证方法包括构造区域自动机和带自动机。通过对这些方法分析研究,我们发现当系统规模较大时,规范建模过程就会相对复杂,而且还可能会出现状态组合爆炸的问题。因此,系统需要一种能较好解决这些问题的自动规范验证技术。 UPPAAL是一种以时间自动机作为行为模型、在实时系统和通讯协议的自动规范验证中占据重要位置的验证工具。在对UPPAAL的基本结构和工作原理分析之后,我们发现它采用的限制技术和快速验证技术可以避免构建状态空间中的不可达状态,能在一定程度上解决状态空间爆炸问题。但是系统在自动规范验证时没能有效利用问题求解过程中的启发性信息,并且存在一些无用状态循环,就会导致问题求解效率低下。本文针对这些问题对快速前向验证算法进行改进,提出了一种带有启发性信息的快速前向验证算法。文中设计估价函数用于估算每一个全局状态到达目标全局状态需要付出的代价,定义无用状态循环用来避免对无用状态重复分析,这样既节省了系统存储空间,又提高了求解问题的效率。接下来,本文对一个通讯协议进行分析和规范,并且利用UPPAAL对该协议的时间自动机模型进行自动规范验证,证明了协议的正确性和安全性。 带有时间特性的Petri网也是一种适合描述和分析实时系统的模型工具,但是它的性能分析能力有一定局限性。因此,本文利用将时延Petri网转换到时间自动机的语义等价转换算法,将一个带有单处理器的铁路岔道系统的时延Petri网模型转换成与其语义等价的一组时间自动机模型,并且利用UPPAAL对转换后系统模型的安全性和受限活性进行自动规范验证。
程永江[7]2009年在《基于时间自动机的模型验证技术》文中进行了进一步梳理随着计算机科学的发展,工业界越来越重视系统的正确性和可靠性,这样使得形式化的模型验证方法得到了广泛地应用。通过可达性分析,模型检测可以完成对实时系统的安全性和活性的验证。它的思想是搜索描述系统行为的转换系统,然后分析可达状态集合,从而确定系统是否满足规格说明。时间自动机是包含时间约束的有限状态转换系统,它是使用最为广泛的形式化验证方法之一。在理论研究部分,首先分析了时间自动机的概念,然后给出了时间自动机的一些扩展形式。实时系统中的事件能否发生对应着时间自动机某个状态从初始状态开始能否可达,因此模型验证主要任务是状态可达性分析。验证需要采用了一些符号化的方法来描述状态,文中首先对时钟区域和时钟带两种方法进行了分析,然后介绍了可达性分析的两种主要的方法。我们重点介绍了基于二元决策图的模型验证方法,而使用它的前提是在时间自动机的整数语义下。详细地解释了如何把整数语义下的状态和转换关系表示成二元决策图的形式。我们给出了在这种数据结构下的可达性分析算法的改进,对该算法进行了时间复杂度分析,并结合一个具体的验证实例对空间复杂度进行了分析,表明改进后的算法的时间复杂度基本不变,同时又降低了可达性分析的空间复杂度。在应用研究部分,首先是介绍了基于时间自动机的验证工具UPPAAL,然后是结合该工具给出了模型验证的步骤和建模的标准,最后构造了飞机着陆控制系统的时间自动机模型,检测了系统是否安全可靠,避免了系统运行时出现错误。通过使用验证工具UPPAAL,我们可以方便地为系统构造模型,有利于设计人员认清系统的运行过程,及时发现系统中存在的一些问题。
石少玲[8]2016年在《基于时间自动机的嵌入式工业控制系统建模与分析》文中提出随着国民经济的发展,实时嵌入式控制系统在工业中得到大量的应用。对实时控制系统的行为进行建模与分析是确保实时控制系统准确性和安全性的重要环节,即输入不同的数据系统能否做出相应的实时响应。时间约束是实时系统的一个重要特点,对于实时计算机系统来说就是系统的很多行为的产生和完成都是与时间相关的。为了保证实时系统的正确性和可靠性,需要对实时系统进行严格的分析和验证,不仅要从逻辑上保证其正确性,而且要求在一定的时间限制内,即时间上的正确性。UML建模工具因为本身具有很强的建模能力从而被广泛地应用在工业控制系统分析和设计中；而时间自动机是目前使用最为广泛的实时系统形式化建模验证工具。本文给出了UML建模的方法以及相应的模型扩展方法,同时也对时间自动机的形式化定义进行了一定的介绍,提出了基于时间自动机的工业控制系统建模方法和工业控制系统向时间自动机自动转化的方法,最后通过对应用实例的实时控制系统进行分析,利用本文提出的UML建模工具和时间自动机模型生成方法对系统的主要场景进行建模,并用时间自动机对建立的模型进行验证和分析。工业控制系统的安全性验证问题和活性问题的验证是工业控制系统建模的关键问题。安全性的验证问题可以转化为时间自动机的可达性分析,活性问题转化成状态的可迁移性。通过本文给出的方法对工业控制系统的实例系统中的一些问题和逻辑或者其他安全隐患进行排查的验证。并通过实验结果分析得出本文的方法能够有效的对系统地正确性和活性问题进行良好的验证。
高冠龙[9]2006年在《基于时间自动机模型验证方法优化研究》文中提出实时系统是一种带有时间约束的计算系统，这些系统的许多动作的完成是与时间相关的，即要满足一定的时间限制。为了确保实时系统的正确性和可靠性，需要对其进行严格的分析和验证。实时系统的验证不仅要求逻辑上是正确的，而且要求时间上也是正确的。现在网络协议的复杂性日益增加。协议中的每一处错误和缺陷都将给网络系统的稳定性、可靠性等带来巨大的危害。协议的验证中往往也需要验证一些时间性质。 对实时系统和协议通常采用形式化的方法来进行验证。有限自动机是最为重要的一种形式描述与验证技术，它是很多形式化方法的基础。它直观性强，可实现与其它形式化方法的组合和转换。但是由于其没有清楚的时间的概念，只能处理事件的序列，而不能准确地描述事件发生的时间，因此在模型验证上的应用受到很大的限制。为解决这个问题，R．Alur等人提出了时间自动机模型。时间自动机存有穷自动机的基础上加入了时钟变量，通过时钟变量和时钟值的比较来约束状态的转移，因此时间自动机可以准确地描述带有时间的系统。 时间自动机的状态空间的大小随着问题规模的增大呈指数级递增。当系统规模较大时，基于时间自动机的验证就会变得非常复杂。所以需要对时间自动机的模型验证方法进行优化。 本文主要研究了域自动机方法、带自动机方法以及基于历史等价和转换互模拟的最小化方法。文中对时钟域及其上的操作给出了一种符号化的表示方法，从而便于域自动机在实际操作中的实现。本文还提出了基于状态转移时间关系的优化方法。该方法通过计算状态转移的最早可能发生时间和最晚可能发生时间来判断转移是否是有效的，通过保留有效转移来简化转换系统。 基于时间自动机已经开发出了多种自动验证工具。这些工具已经在实时系统和协议验证中得到了广泛应用。本文使用Kronos验证了FDDI协议来说明了基于时间自动机的验证过程。
谭耿[10]2008年在《基于UPPAAL的RBC系统控车流程建模分析》文中认为RBC系统是中国铁路CTCS-3级列控系统中的重要组成部分,UPPAAL是基于时间自动机理论的实时系统建模分析验证工具,使用UPPAAL分析RBC系统控车流程,可以验证流程的特性,对于保证RBC系统控车流程的安全性有着重要的实际意义。论文完成的主要工作如下:1.介绍了时间自动机理论及其模型检验工具UPPAAL的使用方法。2.通过分析列车在RBC系统控制下的运行过程,把RBC系统控车流程分为五部分:列车登录流程,正常控车流程,RBC交接流程,列车注销流程和消息重发流程。3.基于时间自动机理论对RBC系统控车的五个流程以及其他外部设备分别进行了建模:根据研究对象的特点,在合理的抽象和假设之后,确定了各个模型的状态,状态跳转路径和状态跳转的约束条件,得到了RBC系统控车流程的时间自动机模型。4.使用UPPAAL对RBC系统控车流程的时间自动机模型进行了分析验证:通过设置通道和全局变量,构造了时间自动机的积;使用模拟器,模拟了RBC控制列车运行过程,分析RBC控制列车运行过程中的状态变化;使用验证器,通过快速搜索整个系统的状态空间,验证RBC系统控车流程的活性和正确性等各项特性。
参考文献：
[1]. 基于时间自动机的实时系统形式化建模与验证[D]. 许丹. 苏州大学. 2007
[2]. 基于时间自动机的CTCS-3级列控系统建模方法与验证研究[D]. 康仁伟. 北京交通大学. 2013
[3]. 基于时间自动机的行车许可的建模与验证[D]. 贺伟. 西南交通大学. 2017
[4]. 基于UPPAAL和UML的实时系统形式化分析与应用[D]. 赵丽芳. 苏州大学. 2008
[5]. 基于时间自动机的实时系统规范验证研究[D]. 姬莉霞. 郑州大学. 2004
[6]. 基于时间自动机的模型验证理论及应用研究[D]. 王静. 郑州大学. 2005
[7]. 基于时间自动机的模型验证技术[D]. 程永江. 郑州大学. 2009
[8]. 基于时间自动机的嵌入式工业控制系统建模与分析[D]. 石少玲. 昆明理工大学. 2016
[9]. 基于时间自动机模型验证方法优化研究[D]. 高冠龙. 郑州大学. 2006
[10]. 基于UPPAAL的RBC系统控车流程建模分析[D]. 谭耿. 北京交通大学. 2008