Timed automata with urgent transitions

We propose an extension to the formalism of timed automata by allowing urgent transitions. An urgent transition is a transition which must be taken within a fixed time interval from its enabling time and it has higher priority than other non-urgent transitions enabled in the same state. We give a set of rules formally describing the behavior of urgent transitions and we show that, from a language theoretic point of view, the addition of urgency does not improve the expressive power of timed automata. From a specification point of view, the use of urgent transitions allows shorter and clear specifications of behaviors involving urgency and priority. We use timed automata with urgent transitions for specifying a multicast protocol for mobile computing.Received: 10 January 2003, Published online: 17 February 2004A first version of this paper appeared in [15]     

一类时间自动机的时间约束可满足性判定方法

时间自动机是一种有效描述实时系统行为的计算模型。借助时间自动机对实时系统进行分析、设计能够保证所开发的实时系统具有较高的可靠性。在此过程中对时间自动机的验证是非常关键的一步。验证的主要目的是为了保证时间自动机能够正确地描述实时系统。其中迁移的时间约束可满足性就是需要验证的性质之一。常用的方法是通过构造时间区域自动机来实现,但该方法所涉及的状态数目巨大。该文针对一类时间自动机的特点给出了基于时间关系矩阵来判定时间约束可满足性的方法,结果表明该方法能够有效地减少状态数。     

Bounded determinization of timed automata with silent transitions

Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. We show how to apply the approach in a fault-based test-case generation method, called model-based mutation testing, that was previously restricted to deterministic timed automata. The approach is implemented in a prototype tool and evaluated on several scientific examples and one industrial case study. To our best knowledge, this is the first implementation of this type of procedure for timed automata.     

Synthesis of Optimal Strategies Using HyTech

Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. The problem of synthesizing an optimal winning strategy for a priced timed game under some hypotheses has been shown decidable in [P. Bouyer, F. Cassez, E. Fleury, and K.G. Larsen. Optimal strategies in priced timed game automata. Research Report BRICS RS-04-4, Denmark, Feb. 2004. Available at http://www.brics.dk/RS/04/4/]. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example.     

The efficiency of identifying timed automata and the power of clocks

We develop theory on the efficiency of identifying (learning) timed automata. In particular, we show that: (i) deterministic timed automata cannot be identified efficiently in the limit from labeled data and (ii) that one-clock deterministic timed automata can be identified efficiently in the limit from labeled data. We prove these results based on the distinguishability of these classes of timed automata. More specifically, we prove that the languages of deterministic timed automata cannot, and that one-clock deterministic timed automata can be distinguished from each other using strings in length bounded by a polynomial. In addition, we provide an algorithm that identifies one-clock deterministic timed automata efficiently from labeled data.Our results have interesting consequences for the power of clocks that are interesting also out of the scope of the identification problem.     

一种基于时间自动机的实时系统测试方法

基于时间自动机(timed automata,简称TA)的一种变体--时间安全输入/输出自动机(timed safety input/output automata,简称TSIOA),提出了一种实时系统测试方法.该方法首先将时间安全输入/输出自动机描述的系统模型转换为不含抽象时间延迟迁移的稳定符号状态迁移图(untimed stable transition graph of symbolic state,简称USTGSS);然后采用基于标号迁移系统(labeled transition system,简称LTS)的测试方法来静态生成满足各种结构覆盖标准的包含时间延迟变量迁移动作序列;最后,给出了一个根据迁移动作序列构造和执行测试用例的过程,该过程引入了时间延迟变量目标函数,并采用线性约束求解方法动态求解迁移动作序列中的时间延迟变量.     

基于时间自动机的测试用例自动生成及执行方法

为了实现对时间自动机模型的测试,采用符号状态拆分算法对时间自动机的状态空间进行等价划分,以得到最简稳定符号状态转移图,并将其中的抽象时间延迟转移替换为时间延迟变量;针对系统中每个时间自动机建立各自的符号状态转移图,再采用基于符号迁移系统的测试方法分别生成相应的转移动作序列;最后通过对这些序列进行组合产生系统的测试用例,为了执行测试用例,利用TTCN-3的多PTC并发执行能力来实施测试.     

A survey of timed automata for the development of real-time systems

Timed automata are a popular formalism to model real-time systems. They were introduced two decades ago to support formal verification. Since then they have also been used for other purposes and a large number of variants has been introduced to be able to deal with the many different kinds of requirements of real-time system development. This survey attempts to introduce a massive and complicated theoretical research area to a reader in an easy and compact manner. One objective of this paper is to inform a reader about the theoretical properties (or capabilities) of timed automata which are (or might be) useful for real-time model driven development. To achieve this goal, this paper presents a survey on semantics, decision problems, and variants of timed automata. The other objective of this paper is to inform a reader about the current state of the art of timed automata in practice. To achieve the second aim, this article presents a survey on timed automata’s implementability and tools.     

Axiomatising timed automata

Timed automata has been developed as a basic semantic model for real time systems. Its algorithmic aspects for automated analysis have been well studied. But so far there is still no satisfactory algebraic theory to allow the derivation of semantical equivalence of automata by purely syntactical manipulation. The aim of this paper is to provide such a theory. We present an inference system of timed bisimulation equivalence for timed automata based on a CCS-style regular language for describing timed automata. It consists of the standard monoid laws for bisimulation and a set of inference rules. The judgments of the proof system are conditional equations of the form where is a clock constraint and t,u are terms denoting timed automata. The inference system is shown to be sound and complete for timed bisimulation. The proof of the completeness result relies on the notion of symbolic timed bisimulation, adapted from the work on value–passing processes. Received: 10 May 2001 / 22 October 2001     

A Kleene–Schützenberger theorem for weighted timed automata

During the last years, weighted timed automata have received much interest in the real-time community. Weighted timed automata form an extension of timed automata and allow us to assign weights (costs) to both locations and edges. This model, introduced by Alur et al. (2001) and Behrmann et al. (2001), permits the treatment of continuous consumption of resources and has led to much research on scheduling problems, optimal reachability and model checking. Also, several authors have derived Kleene-type characterizations of (unweighted) timed automata and their accepted timed languages. The goal of this paper is to provide a characterization of the behaviours of weighted timed automata by rational power series. We define weighted timed automata with weights taken in an arbitrary semiring, resulting in a model that subsumes several weighted timed automata concepts of the literature. For our main result, we combine the methods of Schützenberger, a recent approach for a Kleene-type theorem for unweighted timed automata by Bouyer and Petit as well as new techniques. Our main result also implies Kleene-type theorems for several subclasses of weighted timed automata investigated before, e.g., for timed automata and timed automata with stopwatch observers.     

Symbolic model checking for probabilistic timed automata

Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton’s clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of probabilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies.     

Task automata: Schedulability,decidability and undecidability

We present a model, task automata, for real time systems with non-uniformly recurring computation tasks. It is an extended version of timed automata with asynchronous processes that are computation tasks generated (or triggered) by timed events. Compared with classical task models for real time systems, task automata may be used to describe tasks (1) that are generated non-deterministically according to timing constraints in timed automata, (2) that may have interval execution times representing the best case and the worst case execution times, and (3) whose completion times may influence the releases of task instances. We generalize the classical notion of schedulability to task automata. A task automaton is schedulable if there exists a scheduling strategy such that all possible sequences of events generated by the automaton are schedulable in the sense that all associated tasks can be computed within their deadlines. Our first technical result is that the schedulability for a given scheduling strategy can be checked algorithmically for the class of task automata when the best case and the worst case execution times of tasks are equal. The proof is based on a decidable class of suspension automata: timed automata with bounded subtraction in which clocks may be updated by subtractions within a bounded zone. We shall also study the borderline between decidable and undecidable cases. Our second technical result shows that the schedulability checking problem will be undecidable if the following three conditions hold: (1) the execution times of tasks are intervals, (2) the precise finishing time of a task instance may influence new task releases, and (3) a task is allowed to preempt another running task.     

Accepting Zeno words: a way toward timed refinements

Timed models were introduced to describe the behaviors of real-time systems and they were usually required to produce only executions with divergent sequences of times. However, when some physical phenomena are represented by convergent executions, Zeno words appear in a natural way. Moreover, time can progress if such an infinite execution can be followed by other ones. Therefore, in a first part, we extend the definition of timed automata, allowing to generate sequences of infinite convergent executions, while keeping good properties for the verification of systems: emptiness is still decidable. In a second part, we define a new notion of refinement for timed systems, in which actions are replaced by recognizable Zeno (timed) languages. We study the properties of these timed refinements and we prove that the class of transfinite timed languages is the closure of the usual one (languages accepted by Muller or Büchi timed automata) under refinement. Received: 16 October 1998 / 8 March 2000     

Modeling and verification of real-time embedded systems with urgency

Real-time embedded systems are often designed with different types of urgencies such as delayable or eager, that are modeled by several urgency variants of the timed automata model. However, most model checkers do not support such urgency semantics, except for the IF toolset that model checks timed automata with urgency against observers. This work proposes an Urgent Timed Automata (UTA) model with zone-based urgency semantics that gives the same model checking results as absolute urgency semantics of other existing urgency variants of the timed automata model, including timed automata with deadlines and timed automata with urgent transitions. A necessary and sufficient condition, called complete urgency, is formulated and proved for avoiding zone partitioning so that the system state graphs are simpler and model checking is faster. A novel zone capping method is proposed that is time-reactive, preserves complete urgency, satisfies all deadlines, and does not need zone partitioning. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.     

On model-checking timed automata with stopwatch observers

In this paper, we study the model-checking problem for weighted timed automata and the weighted CTL logic; we also study the finiteness of bisimulations of weighted timed automata. Weighted timed automata are timed automata extended with costs on both edges and locations. When the costs act as stopwatches, we get stopwatch automata with the restriction that the stopwatches cannot be reset nor tested. The weighted CTL logic is an extension of TCTL that allows to reset and test the cost variables. Our main results are: (i) the undecidability of the proposed model-checking problem for discrete and dense time in general, (ii) its PSpace-Completeness in the discrete case, and its undecidability in the dense case, for a slight restriction of the weighted CTL Logic, (iii) the precise frontier between finite and infinite bisimulations in the dense case for the subclass of stopwatch automata.     

An Efficient Algorithm for Minimizing Real-Time Transition Systems

We address the problem of performing simultaneously reachability analysis and minimization of real-time transition systems represented by timed automata, i.e., automata extended with a finite set of clock variables. The transitions of the automaton may depend on the values of the clocks and may reset some of the clocks. An efficient algorithm is presented for minimizing a system with respect to a given initial partition that respects the enabling conditions of the transitions of the timed automaton. Our algorithm generates the portion of the minimized system that is reachable from a given initial configuration in time polynomial in the input and the size of the minimal reachable system.     

一种基于时间自动机的域构造方法

模型检验是一种重要的形式化自动验证技术,通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机,而是针对有限状态变迁系统的,从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法,并在不改变时间自动机的语义上,使时间自动机等价后的域状态数尽可能少,在一定程度上有效地解决了状态空间爆炸问题。     

Diagnosis of timed automata: Theory and application to the DAMADICS actuator benchmark problem

This paper concerns the problem of fault diagnosis in discrete-event systems which are represented by timed automata. The diagnostic algorithm for timed automata detects and identifies faults in the system based on the investigation whether the measured input and output sequences are consistent with the timed automaton. This diagnostic approach can be applied spontaneously to the discrete-event system since no a priori information about the initial state of the system is required. It is shown in the paper how the timed automaton which represents the DAMADICS actuator can be obtained and how the diagnostic algorithm based on the timed automaton is applied to detect and identify actuator faults. A representative diagnostic result is presented and discussed to illustrate the effectiveness of the method.     

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

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