基于时间自动机的实时系统建模及验证

实时系统必须在一个事先定义好的时间限制内对来自外部或内部的事件进行响应,如何有效验证实时模型的正确性和安全性是一个难点.文章通过多个时间自动机来模拟实时系统中的各个对象,并用UPPAAL对模型进行验证,减少了模型验证的状态搜索空间,为实时嵌入式系统开发和验证提供了一种可行、安全的控制机制.实验结果显示了系统的有效性.     

基于时间自动机的AADL端到端流规约验证方法

体系结构分析及设计语言(AADL)作为一种标准且直观的实时系统分析与设计工具,可以为系统设计、分析、验证、自动代码生成等关键环节提供统一的抽象表示。然而,AADL模型采用仿真的验证方法无法得到精确的端到端延迟验证结果,尤其是对于资源动态分配的实时系统。为解决结果不精确的问题,可结合基于系统有穷状态空间遍历的模型检验方法。首先,将实时系统AADL模型转换为时间自动机(TA)模型,以TA为理论体系进行模型检验。其次,基于反应链的需求分类定义端到端延迟需求表达模式。最后,给出对应需求模式的观察者模型,与系统模型并行组合,优化模型验证的时空资源消耗。     

时间自动机与网络协议验证

随着网络协议复杂性的增大，其自身的潜在错误变得更加重要。使用形式化的方法来描述和验证网络协议可以发现其中的潜在错误。时间自动机是形式化方法的一种，可以很好地应用于网络协议验证中。目前基于时间自动机已经开发出了多种自动验证工具。文章介绍了网络协议验证的几种方法，并以KRONOS验证FDDI协议为例说明了用时间自动机验证协议的方法。     

混杂系统的扩展时间自动机模型及验证研究

混杂系统复杂度高且涉及领域广,没有通用的方法来解决分析、设计等问题。为解决一类工业控制混杂系统的建模和验证问题,对时间自动机进行了语义扩展,使其含有连续变量以及映射在其上的约束,使用扩展后的时间自动机对此类混杂系统进行建模,采用验证工具UPPAAL进行模型分析模拟,并使用简化的CTL对系统需求规范进行验证。具体实例研究表明,该方法对于分析设计一类混杂系统具有可行性和有效性。     

基于uppaal的飞机着陆控制系统模型验证

为了避免飞机在着陆过程中出现事故,同时又能充分利用机场的跑道资源,对飞机数量多于跑道的情况进行了研究,采用了模型验证的方法.介绍了时间自动机的相关理论,以及基于该理论的验证工具uppaal,在此基础上使用uppaal工具对飞机着陆过程构造了模型,然后对模型的需求规范进行了验证,验证结果表明该模型不存在死锁问题,最终可以保证飞机安全和及时地着陆.     

一种基于时间自动机的实时系统模型检查算法的设计与实现

该文首先简介了时间自动机、时钟区域、区域等价、时钟带的概念,利用区域等价关系,可以将时间自动机的无穷状态空间转化为有穷。然后通过一个典型的实例完整地介绍了基于时间自动机的实时系统模型检查技术,并用Visual C++语言描述了实时特性验证中的数据结构,实现了实时特性验证算法,实验表明利用该算法可以进行实时系统的形式化验证。     

一种基于有限精度时间自动机的模型检测工具

基于有限精度时间自动机模型,实现了一种新的数据结构——SDS ,用SDS 符号化表示状态空间的实时系统模型检测工具,并进行了初步的实验分析,取得了良好的效果。     

基于时间自动机的物联网服务建模和验证

物联网服务的建模和验证是当前物联网服务提供中的一个重要问题.文中将物联网服务的行为建模为其与相关环境实体的交互,并引入环境实体以刻画物理世界各种物体的属性和行为,从而将物联网服务能力建模为它能够导致的环境实体发生的期望变化.文中以时间自动机为建模工具,分别为将要监测和要控制的物理环境实体以及不同种类的物联网服务独立建模...     

基于IF的实时系统验证

IF是一个对异步实时系统建模和验证的开放环境,建立在具有丰富表达能力,基于时间自动机的中间语言IF符号集之上。文章描述了IF的组成,包括其体系结构,所使用的符号集;然后给出了IF对实时系统验证的方法,并运用此验证方法对一个实时系统实例进行了验证。     

基于时间自动机模型的测试用例生成方法优化

为了减少测试产生、执行,存储以及维护测试用例的代价,提出了一种基于时间自动机模型的测试用例生成方法的优化技术.针对实时系统中不同的时间尺度,为了加快基于模型的测试用例生成的速度,通过对原时间自动机模型的结构进行改进,对这类实时系统进行测试产生优化.实验结果表明,优化后产生的测试用例集的大小及所用时间相对于优化之前有较大程度的约减,为进一步减少测试执行的时间,提高测试效率,加快软件开发进程提供了可行的解决途径.     

实例化过程模型的时间自动机描述方法研究

语法结构正确的过程模型并不能保证过程运作的实际执行,因为没有考虑实例化阶段的时间资源安排.传统的过程自动机描述法不足以分析实例化过程模型.针对这种情况,提出用时间自动机描述过程模型语义的方法,设计了生成时间自动机的算法,分析了这种描述方法在模型检验中的应用.     

Uppaal到PVS的时间自动机翻译器

Uppaal是一种对实时系统模型进行建模和验证的工具,PVS（Prototype Verification System）是开发和分析形式化规格说明的原型证明系统。介绍了Uppaal2PVS翻译器的设计与实现,给出了一种将用Uppaal生成的时间自动机规格说明翻译成PVS文件的方法,从而将模型检查问题转换成了定理证明问题,解决了潜在的状态空间爆炸问题。最后给出了一个实例。     

基于on-the-fly的Petri网模型检查技术研究与实现

Petri网是一种应用非常广泛的建模工具,它能深刻、简洁地描述控制系统,特别是能较好地描述并发系统的结构,并能对系统的动态性质进行分析。在探讨了Petri网的模型检查的基础上,采用双DFS算法,对基于Petri网的模型检查的算法进行了改进,提出了针对Petri网的on-the-fly算法,同时给出了基于on-the-fly的Petri网模型检查的实现和测试,从而可以有效地对Petri网表示的系统模型进行模型检查。     

实时系统时段性质的模型检验

一、前言随着计算机硬件的飞速发展,计算能力和速度大幅度提高,一方面使得计算机技术应用范围不断扩大,另一方面使得计算机系统的规模和复杂性急剧增加,导致系统出错的几率也随之增大。但任何一个错误在某些系统,如:空中运输控制系统、银行财务系统等,往往可能导致重大的经济损失,甚至人员伤亡,如1996年阿波罗5号火箭的爆炸等。显然对这种高安全性系统的正确性要求是极其严格的,在高安全性系统的开发过程中,最为关键的问题是如何在尽可能早的阶段验证设计的正确性。应用计算机系统的最大障碍就是系统的正确性无法保证,因此提高系统的正确性与可靠性变得日益迫切。     

模型检测在软件需求分析及设计中的应用

模型检测技术因其完全自动化并且验证速度快的优点在硬件及协议的验证中广泛应用,近年来在软件领域的应用研究也不断涌现.总结了模型检测在软件需求分析及设计中已有的应用技术,包括利用模型检测工具对RSML,SCR和UML图形的检测,以及直接的模型检测,并从不同角度对已有技术进行系统的分析和比较.最后对该项技术研究的方向进行展望.     

面向媒体时序描述的带时间自动机的自动构造方法

依据有穷状态自动机模型,面向程序规范的并发系统和分布式系统测试方法的研究已经取得许多结果。由于特殊的实时和同步要求,这些结果不能直接应用于分布式多媒体软件系统的测试。为此,作者提出一种面向媒体对象时序描述的地间自动机（Ｔｉｍｅｄ ａｕｔｏｍａｔａ）的自动构造方法,根据带时间自动机,对分布式多媒体软件系统进行非确定性测试时,可以较容易地判断运行结果正确与否;在进行确定性测试时,可以辅助自动生成测试用     

UML可视化建模工具中模型一致性检查机制的研究与实现

采用统一建模语言UML进行系统建模的过程中,模型一致性的建立和维护是正确建模的必要前提。但单靠人工检查的方式来保证模型的正确性,不仅给开发人员造成很大负担,而且容易出现差错或遗漏。因此,在UML可视化建模工具中提供模型一致性自动检测和维护机制至关重要。本文对UML主要模型图之间的关系进行了分析,识别出这些图之间的一些基本的一致性规则;在此基础上,提出了UML可视化建模工具中模型一致性检查机制的实施框架,并对实现该框架的主要思路进行了详细介绍。     

Validating timed UML models by simulation and verification

This paper presents a technique and a tool for model-checking operational (design level) UML models based on a mapping to a model of communicating extended timed automata. The target language of the mapping is the IF format, for which existing model-checking and simulation tools can be used. Our approach takes into consideration most of the structural and behavioural features of UML, including object-oriented aspects. It handles the combination of operations, state machines, inheritance and polymorphism, with a particular semantic profile for communication and concurrency. We adopt a UML profile that includes extensions for expressing timing. The breadth of concepts covered by our mapping is an important point, as many previous approaches for applying formal validation to UML put much stronger limitations on the considered models. For expressing properties about models, a formalism called UML observers is defined in this paper. Observers reuse existing concepts like classes and state machines, and they allow expressing a significant class of linear temporal properties. The approach is implemented in a tool that imports UML models from an XMI repository, thus supporting several editors like Rational Rose, Rhapsody or Argo. The generated IF models may be simulated and verified via an interface that presents feedback in the vocabulary of the original UML model. This work has been partially supported by the OMEGA European Project (IST-33522). See also http://www-omega.imag.fr     

Timed verification of the generic architecture of a memory circuit using parametric timed automata

Using a variant of Clariso-Cortadella’s parametric method for verifying asynchronous circuits, we analyse some crucial timing behaviors of the architecture of SPSMALL memory, a commercial product of STMicroelectronics. Using the model of parametric timed automata and model checker HYTECH, we formally derive a set of linear constraints that ensure the correctness of the response times of the memory. We are also able to infer the constraints characterizing the optimal setup timings of input signals. We have checked, for two different implementations of this architecture, that the values given by our model match remarkably with the values obtained by the designer through electrical simulation. Partially supported by project MEDEA+ Blueberries. A preliminary version appeared in the Proceedings of 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS’06), Sept. 2006.     

并发和实时系统的模型检验技术

模型检验是一种重要的自动验证技术,通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态／命题性质,以保证通信协议、数字电路等设计的正确性。详细阐述了模型检验技术的发展与研究现状。首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略,并给出解决状态爆炸问题的主要方法;然后介绍了针对实时系统以及面向对象设计的模型检验方法;对每种方法都介绍了相应的典型工具,最后分析了模型检验面临的困难以及今后的发展趋势。