| 1. |
- Amnell, Tobias, et al.
(författare)
-
Code Synthesis for Timed Automata
- 2002
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 9:4, s. 269-300
-
Tidskriftsartikel (refereegranskat)
|
|
| 2. |
- Amnell, Tobias, et al.
(författare)
-
Code Synthesis for Timed Automata
- 2002
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a framework for development of real-time embedded systems based on the recently presented model of timed automata extended with real-time tasks. It has been shown previously that design problems such as reachability and schedulability are decidable for the model of timed automata with tasks. In this paper we describe how to automatically synthesise executable code with predictable timing behaviour, which is guaranteed to meet constraints (timing and other) imposed on the design model. To demonstrate the applicability of the framework, implemented in the Times tool, we present a case-study of a well known production cell, built in LEGO and controlled by a Hitachi H8 based LEGO Mindstorm control brick.
|
|
| 3. |
|
|
| 4. |
|
|
| 5. |
- Amnell, Tobias, et al.
(författare)
-
TIMES: a Tool for Schedulability Analysis and Code Generation of Real-Time Systems
- 2003
-
Ingår i: Proceedings of the International Conference of Formal Modeling and Analysis of Timed Systems. - 9783540216711
-
Konferensbidrag (refereegranskat)abstract
- TIMES is a tool suite designed mainly for symbolic schedulability analysis and synthesis of executable code with predictable behaviours for real-time systems. Given a system design model consisting of(1) a set of application tasks whose executions may be required to meet mixed timing, precedence, and resource constraints,(2) a network of timed automata describing the task arrival patterns and(3) a preemptive or non-preemptive scheduling policy,TIMES will generate a scheduler, and calculate the worst case response times for the tasks. The design model may be further validated using a model checker e.g. UPPAAL and then compiled to executable C-code using the TIMES compiler. In this paper, we present the design and main features of TIMES including a summary of theoretical results behind the tool. TIMES can be downloaded at www.timestool.com.
|
|
| 6. |
|
|
| 7. |
|
|
| 8. |
- Fersman, Elena, 1978-
(författare)
-
A Generic Approach to Schedulability Analysis of Real-Time Systems
- 2003
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- This thesis presents a framework for design, analysis, and implementation of embedded systems. We adopt a model of timed automata extended with asynchronous processes i.e. tasks triggered by events. A task is an executable program characterized by its worst-case execution time and deadline, and possibly other parameters such as priorities etc. for scheduling. The main idea is to associate each location of an automaton with a task (or a set of tasks). A transition leading to a location denotes an event triggering the tasks and the clock constraint on the transition specifies the possible arrival times of the event. This yields a model for real-time systems expressive enough to describe concurrency and synchronization, and tasks with (or without) combinations of timing, precedence and resource constraints, which may be periodic, sporadic, preemptive and (or) non-preemptive. We believe that the model may serve as a bridge between scheduling theory and automata-theoretic approaches to system modelling and analysis. Our main result is that the schedulability checking problem for this model is decidable. To our knowledge, this is the first general decidability result on dense-time models for real time scheduling without assuming that preemptions occur only at integer time points. The proof is based on a decidable class of updatable automata: timed automata with subtraction in which clocks may be updated by subtractions within a bounded zone. As the second contribution, we show that for fixed priority scheduling strategy, the schedulability checking problem can be solved by reachability analysis on standard timed automata using only two extra clocks in addition to the clocks used in the original model to describe task arrival times. The analysis can be done in a similar manner to response time analysis in classic Rate-Monotonic Scheduling. We believe that this is the optimal solution to the problem. The third contribution is an extension of the above results to deal with precedence and resource constraints. We present an operational semantics for the model, and show that the related schedulability analysis problem can be solved efficiently using the same techniques. Finaly, to demonstrate the applicability of the framework, we have modelled, analysed, and synthesised the control software for a production cell. The presented results have been implemented in the Times tool for automated schedulability analysis and code synthesis.
|
|
| 9. |
|
|
| 10. |
|
|
| 11. |
|
|
| 12. |
|
|
| 13. |
- Fersman, Elena, et al.
(författare)
-
Schedulability Analysis using Two Clocks
- 2003
-
Ingår i: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. - 9783540008989
-
Konferensbidrag (refereegranskat)abstract
- In classic scheduling theory, real-time tasks are usually assumed tobe periodic, i.e. tasks arrive and compute with fixed ratesperiodically. To relax the stringent constraints on task arrivaltimes, we propose to use timed automata to describe task arrivalpatterns. In a previous work, it is shown that the generalschedulability checking problem for such models is a reachabilityproblem for a decidable class of timed automata extended withsubtraction. Unfortunately, the number of clocks needed in theanalysis is proportional to the maximal number of schedulable taskinstances associated with a model, which in many cases is huge.In this paper, we show that for fixed priority scheduling strategy,the schedulability checking problem can be solved by reachabilityanalysis on standard timed automata using only two extra clocksin addition to the clocks used in the original model to describe taskarrival times. The analysis can be done in a similar manner toresponse time analysis in classic Rate-Monotonic Scheduling.We believe that this is the optimal solution to the problem,a problem that was suspected undecidable previously.We also extend the result to systems in which the timed automata and the tasks may read and update shared data variables. Then the release time-point of a task may depend on the values of the shared variables, and hence on the time-point at which other tasks finish their exection. We show that this schedulability problem can be encoded as timed automata using n+1 extra clocks, where n is the number of tasks.
|
|
| 14. |
- Fersman, Elena, et al.
(författare)
-
Timed Automata with Asynchronous Processes : Schedulability and Decidability
- 2002
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we exend timed automata with asynchronous processes i.e. tasks triggered by events as a model for real-time systems. The model is expressive enough to describe concurrency and synchronization, and real time tasks which may be periodic, sporadic, preemptive or non-preemptive. We generalize the classic notion of schedulability to timed automata. An automaton is schedulable if there exists a scheduling strategy such that all possible sequences of events accepted by the automaton are schedulable in the sense that all associated tasks can be computed within their deadlines. We believe that the model may serve as a bridge between scheduling theory and automata-theoretic approaches to system modeling and analysis. Our main result is that the schedulability checking problem is decidable. To our knowledge, this is the first general decidability result on dense-time models for real time scheduling without assuming that preemptions occur only at integer time points. The proof is based on a decidable class of updatable automata: timed automata with subtraction in which clocks may be updated by subtractions within a bounded zone. The crucial observation is that the schedulability checking problem can be encoded as a reachability problem for such automata. Based on the proof, we have developed a symbolic technique and a prototype tool for schedulability analysis.
|
|
