共查询到19条相似文献,搜索用时 234 毫秒
1.
XYZ系统是一个以增强软件可靠性和提高软件生产率为目的的程序开发支撑系统.它由时序逻 辑语言(temporal logic language,简称TLL)XYZ/E和以该语言为基础的一组软件工程工具组 成.为了研究XYZ系统在多媒体领域中的应用问题,介绍了一种依据多媒体对象时序描述 自动生成用XYZ/RE表示的播放同步器的方法,XYZ/RE是时序逻辑语言族XYZ/E中表示实时系统 的子语言.与相关工作比较,该方法不仅可以处理简单的时序关系,而且可以处理嵌套的时序 关系,所产生的同步器可以复用于不同的节目. 相似文献
2.
3.
时延Petri网和时间自动机都可以有效地对实时系统的行为进行模拟和性能分析。利用时延Petri网到时间自动机等价转换算法(简记作TPN-to-TA 转换),将一个描述实时系统的时延Petri网模型转换成与其语义等价的一组时间自动机模型。使用时间自动机中成熟的模型验证工具Uppaal对此时延Petri网的模型进行验证。 相似文献
4.
使用时间化自动机形式化带有时间扩展的UML状态图 总被引:9,自引:0,他引:9
严格建模是嵌入式实时系统设计的核心技术,通过UMI。方法与形式化方法结合可以给严格建模提供很好的工具支持。时间化自动机(Timed Automata)是一种用于描述、验证实时系统的理论模型。文中提出了一种通过时间化自动机来形式化带有时间扩展的UML状态图的方法,这种方法为UMI。与形式化方法的结合构造了桥梁作用。带有时间扩展的UML状态图用于嵌入式系统动态模型的建模,从时间化自动机模型得到形式化规范将更容易。UML状态图的形式化分为两部分完成;层次状态图的平面化以及时间化自动机的构造。 相似文献
5.
自动验证并发实时系统的线性时段性质 总被引:1,自引:0,他引:1
介绍了一个就线性时段性验证实时系统正确性的工具的设计思想以及相关算法,使用时间自动机作为产时系统的描述模型,同时,为了便珩描述并发实时系统,使用带共享变量和通道的时间自动机网作为模型描述并发实时系统,在检验时间自动机网时,用户可以使用工具提供的合成程序将其合并为一个时间自动机然后进行检验,由于时间自动机的状态空间是无究的,通过引入整数状态和状态等价关系的概念,将整个状态0空间划分为有限的状态等价类空间,模型检验过程只需要通过对等价类空间的搜索就可以完成,但往往等价类空间的规模很大,超出了现在计算机的处理能力,原始搜索算法仅仅在理论上是可知地的,为了增工具的使用性,工具中使用的算法运用了一些优化技术来避免对等价类空间的穷尽搜索,使得工具在使用时具有比较好的时间和空间效率。 相似文献
6.
7.
王勤思 《计算机工程与设计》2011,32(2):568-571,575
在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B chi自动机。这样扩展了已有实时系统模型检测工具的性质规范语言的表达能力,使其能直接处理和验证带有明显时间约束的性质。实现的工具表明,该算法有效且可行,并且显著地减少了结果自动机节点和迁移的数量,从而降低了结果自动机的大小,有利于进一步的模型检测过程。 相似文献
8.
时间自动机是一种有效描述实时系统行为的计算模型。借助时间自动机对实时系统进行分析、设计能够保证所开发的实时系统具有较高的可靠性。在此过程中对时间自动机的验证是非常关键的一步。验证的主要目的是为了保证时间自动机能够正确地描述实时系统。其中迁移的时间约束可满足性就是需要验证的性质之一。常用的方法是通过构造时间区域自动机来实现,但该方法所涉及的状态数目巨大。该文针对一类时间自动机的特点给出了基于时间关系矩阵来判定时间约束可满足性的方法,结果表明该方法能够有效地减少状态数。 相似文献
9.
10.
目前,能够对汽车电子领域中复杂嵌入式系统安全关键软件功能模和时间约束分析的方法尚在研究中,而这些系统作为实时控制系统,应该确保其具有准确的、可分析的时间行为。时钟约束规范语言CCSL是实时系统的标准描述语言中描述时钟约束的规范语言。采用CCSL规范表达式描述实时系统时间约束;设计了CCSL基本元素到时间自动机基本元素的转换规则;使用时间自用机验证工具UPPAAL对转换得到的自动机模型进行验证分析,验证实时系统是否满足相应的时间约束。 相似文献
11.
Dong Jin Song Hao Ping Qin Shengchao Sun Jun Yi Wang 《IEEE transactions on pattern analysis and machine intelligence》2008,34(6):844-859
Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been developed. However, Timed Automata lack of composable patterns for high-level system design. Logic-based specification languages like Timed CSP and TCOZ are well suited for presenting compositional models of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchical constructs in timed enriched process algebras. The patterns facilitate hierarchical design of complex systems using Timed Automata. They also allow a systematic translation from Timed CSP/TCOZ models to Timed Automata so that analyzers for Timed Automata can be used to reason about TCOZ models. A prototype has been developed to support system design using Timed Automata patterns or, if given a TCOZ specification, to automate the translation from TCOZ to Timed Automata. 相似文献
12.
模型驱动体系结构(MDA)是一种以模型为中心的软件开发框架,其本质是元建模与模型转换。提出了一种基于MDA的实时软件资源建模与模型转换的方法。首先通过元建模抽象出包含资源信息的MARTS元模型以及价格时间自动机的元模型;然后利用模型转换语言ATL对MARTS元模型和价格时间自动机元模型构造转换规则,通过将对应的实例模型进行相互转换,实现在MDA下MAR"I'E模型到价格时间自动机模型的转换;最后通过形式化工具UPPAAL对模型转换结果进行形式化验证。实例分析表明了该方法的可行性与有效性,它能够提高实时软件资源建模的可信性。 相似文献
13.
Michael R. Hansen 《Formal Aspects of Computing》1994,6(1):826-845
Duration Calculus was introduced in [ZHR91] as a logic to specify and reason about requirements for real-time systems. It is an extension of Interval Temporal Logic [Mos85] where one can reason about integrated constraints over time-dependent and Boolean valued states without explicit mention of absolute time. Several major case studies, e.g. the gas burner system in [RRH93], have shown that Duration Calculus provides a high level of abstraction for both expressing and reasoning about specifications. Using Timed Automata [A1D92] one can express how real-time systems can be constructed at a level of detail which is close to an actual implementation. We consider in the paper the correctness of Timed Automata with respect to Duration Calculus formulae. For a subset of Duration Calculus, we show that one can automatically verify whether a Timed Automaton ? is correct with respect to a formulaD, abbreviated ? ?D, i.e. one can domodel-checking. The subset we consider is expressive enough to formalize the requirements to the gas burner system given in [RRH93]; but only for a discrete time domain. Model-checking is done by reducing the correctness problem ? ?D to the inclusion problem of regular languages. 相似文献
14.
15.
Guillaume Gardey John Mullins Olivier H. Roux 《Electronic Notes in Theoretical Computer Science》2007,180(1):35
In this paper, the problem of synthesizing controllers that ensures non interference for multilevel security dense timed discrete event systems modeled by an extension of Timed Automata, is addressed for the first time. We first discuss a notion of non interference for dense real-time systems that refines notions existing in the literature and investigate decidability issues raised by the verification problem for dense time properties. We then prove the decidability of the problem of synthesis of the timed controller for some of these timed non interference properties, providing so a symbolic method to synthesize a controller that ensures them. 相似文献
16.
Model-checking discrete duration calculus 总被引:1,自引:0,他引:1
Michael R. Hansen 《Formal Aspects of Computing》1994,6(6):826-845
Duration Calculus was introduced in [ZHR91] as a logic to specify and reason about requirements for real-time systems. It is an extension of Interval Temporal Logic [Mos85] where one can reason about integrated constraints over time-dependent and Boolean valued states without explicit mention of absolute time. Several major case studies, e.g. the gas burner system in [RRH93], have shown that Duration Calculus provides a high level of abstraction for both expressing and reasoning about specifications. Using Timed Automata [A1D92] one can express how real-time systems can be constructed at a level of detail which is close to an actual implementation. We consider in the paper the correctness of Timed Automata with respect to Duration Calculus formulae. For a subset of Duration Calculus, we show that one can automatically verify whether a Timed Automaton is correct with respect to a formulaD, abbreviated D, i.e. one can domodel-checking. The subset we consider is expressive enough to formalize the requirements to the gas burner system given in [RRH93]; but only for a discrete time domain. Model-checking is done by reducing the correctness problem D to the inclusion problem of regular languages. 相似文献
17.
18.
基于有限精度时间自动机模型,实现了一种新的数据结构——SDS ,用SDS 符号化表示状态空间的实时系统模型检测工具,并进行了初步的实验分析,取得了良好的效果。 相似文献
19.
时间动作锁(Ti me-Action-Lock,TAL)指的是实时系统处于一种时间无法继续同时又没有任何动作能够发生的状态.Behzad和Kozo在时间自动机的几何学基础上提出了一种针对TAL-freeness的检测方法.但该方法要求必须将需要检测的模型转化为一种逻辑语言Rational Presburger Sentences后才能进行检测,因此使得验证过程比较繁琐.文中提出了一种检测TAL-freeness的代数方法,能够直接对系统模型进行直接验证,并且能够定位死锁原因.针对该方法,文中还给出了相应算法并提供了正确性证明与性能分析. 相似文献