| 1. |
|
|
| 2. |
- Amnell, Tobias, et al.
(author)
-
Code Synthesis for Timed Automata
- 2002
-
In: Nordic Journal of Computing. - 1236-6064. ; 9:4, s. 269-300
-
Journal article (peer-reviewed)
|
|
| 3. |
- Amnell, Tobias
(author)
-
Code synthesis for timed automata
- 2003
-
Licentiate thesis (other academic/artistic)abstract
- In this thesis, we study executable behaviours of timed models. The focus is on synthesis of executable code with predictable behaviours from high level abstract models. We assume that a timed system consists of two parts: the control software and the plant (i.e. the environment to be controlled). Both are modelled as timed automata extended with real time tasks. We consider the extended timed automata as design models.We present a compilation procedure to transform design models to executable code including a run-time scheduler (run time system) preserving the correctness and schedulability of the models. The compilation procedure has been implemented in a prototype C-code generator for the brickOS operating system included in the Times tool. We also present an animator, based on hybrid automata, to be used to describe a simulated environment (i.e. the plant) for timed systems. The tasks of the hybrid automata define differential equations and the animator uses a differential equations solver to calculate step-wise approximations of real valued variables. The animated objects, described as hybrid automata, are compiled by the Times tool into executable code using a similar procedure as for controller software.To demonstrate the applicability of timed automata with tasks as a design language we have developed the control software for a production cell. The production cell is built in LEGO and is controlled by a Hitachi H8 based LEGO-Mindstorms control brick. The control software has been analysed (using the Times tool) for schedulability and other safety properties. Using results from the analysis we were able to avoid generating code for parts of the design that could never be reached, and could also limit the amount of memory allocated for the task queue.
|
|
| 4. |
- Amnell, Tobias, et al.
(author)
-
Code Synthesis for Timed Automata
- 2002
-
Reports (other academic/artistic)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.
|
|
| 5. |
|
|
| 6. |
|
|
| 7. |
- Amnell, Tobias, et al.
(author)
-
TIMES: a Tool for Schedulability Analysis and Code Generation of Real-Time Systems
- 2003
-
In: Proceedings of the International Conference of Formal Modeling and Analysis of Timed Systems. - 9783540216711
-
Conference paper (peer-reviewed)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.
|
|
| 8. |
|
|
| 9. |
|
|
