Scheduling and control generation with environmental constraints based on automata representations
15
Citation
32
Reference
10
Related Paper
Abstract:
We introduce a framework for synthesis of behavioral models in which design information is represented using an automaton model. This model offers the advantage of supporting different constraints (e.g., timing, resource, synchronization, etc.) with a uniform formalism. The set of all feasible execution traces (schedules) is constructed and traversed using efficient BDD-based implicit state-traversal techniques. As an application example of this formalism, we present a novel scheduling/control-generation algorithm under environmental constraints where both the design and constraints are represented using automata. We present an algorithm that generates a minimum-latency schedule and a control unit representation. This approach is able to exploit degrees of freedom among interacting components of a multimodule system during scheduling, and is well suited for system-level design, where component encapsulation and interfacing are important.Timed automaton
TRACE (psycholinguistics)
Cite
Citations (33)
Multirate timed automata are an extension of timed automata where each clock has its own speed varying between a lower and an upper bound that may change from one control location to another. This formalism is well-suited for specifying hybrid systems where the dynamics of the continuous variables are defined or can be approximated by giving the minimal and maximal rate of change. To avoid the difficulties inherent in the verification of multirate timed automata, we follow an approach that consists of first transforming the multirate timed automata into timed automata and then applying the symbolic techniques implemented in KRONOS. We show the practical interest of this approach analyzing two examples recently proposed in the literature and considered to be realistic case studies: a manufacturing plant and the Philips audio control protocol.
Timed automaton
Formalism (music)
Hybrid automaton
Cite
Citations (125)
We show that timed automata can be used to model and to analyze timeliness properties of embedded system architectures. Using a case study inspired by industrial practice, we present in detail how a suitable timed automata model is composed. Exact upper bounds on the timeliness properties can be found with the Uppaal model checker for a number of usage scenarios. We compare our results with three other performance modeling techniques. This comparison shows that if the state space of the model is tractable, Uppaal gives the most accurate results at similar cost. The proposed modeling strategy can be automated, which alleviates the difficulty and error-proneness of manually constructing timed automata models
Timed automaton
Cite
Citations (54)
This paper deals with the problem of temporal coherence when timed automata composition is achieved. The automata models used are based on those of Alur and Dill (1994). The composition is quasi-similar to the one for untimed automata, nevertheless the conjunction of guards must be added on every transition. Even if this composition, as any composition, solves the automata event dependence problem, this is not the case as far as temporal dependence is concerned. The purpose of this paper is to present the problem and to propose a method putting forward the possible temporal incoherence for the automaton resulting from the composition, in view of use in the supervisory control framework. Two examples illustrate the method.
Timed automaton
Cite
Citations (2)
Abstract: In this contribution, we study the performances of discrete event systems modeled by (max,+) automata. More precisely, new representations for (max,+) automata are first proposed. From these, several performance indicators can be derived, in particular the maximum time execution and a minorant of the minimum execution time for a sequence of length n. Finally these results are discussed in comparison with several studies of the literature also dealing with performance evaluation of (max,+) automata.
Sequence (biology)
Learning Automata
Discrete-Event Simulation
Cite
Citations (0)
This note corrects a technical error in the ACM Computing Surveys paper mentioned in the title. The flaw involved constructions for showing that timed automata with urgent locations have the same expressiveness as timed automata that allow false location invariants. Corrected con- structions are presented in this note, and the affected results are reproved.
Menagerie
Timed automaton
Cite
Citations (0)
This note corrects a technical error in the ACM Computing Surveys paper mentioned in the title. The flaw involved constructions for showing that timed automata with urgent locations have the same expressiveness as timed automata that allow false location invariants. Corrected con- structions are presented in this note, and the affected results are reproved.
Menagerie
Timed automaton
Cite
Citations (0)
MONA implements an efficient decision procedure for the logic WS1S, and has already been applied in many non-trivial problems. Among these, we follow on from previous work done by Smith and Klarlund on the verification of a sliding-window protocol. One of the goals of this paper is to extend the scope of MONA to the verification of time-dependent protocols. We present Discrete Timed Automata (DTA) as a suitable formalism to specify and verify such protocols, and (discrete, infinite-state) real-time systems in general. DTA are as much influenced by IO Automata (syntactically) as they are by Timed Automata (semantically). However, DTA presents a number of distinctive features. Among them, urgency conditions can be directly related to actions, and they are constrained in such a way that time-actionlocks are ruled out by construction. A composition strategy is given to combine a set of synchronising automata, resulting in a product automaton over which safety properties can be verified. Invariance proofs are then performed inductively on the automaton structure, and mechanically assisted by MONA. Therefore, this paper also aims to study benefits and weaknesses of DTA as a real-time formalism, compared with existent frameworks such as Timed IO Automata, TLA+ and Clocked Transition Systems. Our case study will be the specification and verification of a multimedia stream protocol. This is compared to previous work where the formalisation of the protocol is realised in UPPAAL.
Timed automaton
Formalism (music)
Cite
Citations (5)
We show that timed automata can be used to model and to analyze timeliness properties of embedded system architectures. Using a case study inspired by industrial practice, we present in detail how a suitable timed automata model is composed. Exact upper bounds on the timeliness properties can be found with the Uppaal model checker for a number of usage scenarios. We compare our results with three other performance modeling techniques. This comparison shows that if the state space of the model is tractable, Uppaal gives the most accurate results at similar cost. The proposed modeling strategy can be automated, which alleviates the difficulty and error-proneness of manually constructing timed automata models.
Timed automaton
Cite
Citations (73)