- A tool environment for the development of embedded systems
- Project no: A6-9805
- Christer Norström and Wang Yi
- Mälardalen University, Computer Engineering Department, MRTC
- Application as pdf, support letter from Mecel AB.
- Application for prologation 01-08-10, support letter 1 from Systemite AB and support letter 2 Bombardier Transportation.
- Support: 1 PhD student for 2 years decided 98-06-03.
- Start 99-01-01 with Anders Wall as PhD student.
- Reports: Progress page, Updated project plan as pdf , ps. Report 000313.
1-year-report 00-06-06, Second-year-report
- Project web: http://www.docs.uu.se/~yi/ARTES/scheduling/home.html
- Lars Magnusson email@example.com
- Mecel AB
- Project 1: A tool environment for the development of embedded systems
- Project 2: Identification of Complexity-Reduction Techniques for Optimal Scheduling in Embedded Distributed Real-Time Systems
- Project 3: Hierarchical Design and Analysis of Timed Systems
- Project 4: Flexible reliable timing constraints
- Project 5: RATAD,
Reliability And Timing Analysis of Distributed systems
- Project 6: Extension of Project Flexible Reliable
This project was started in January, 1999 . One Ph.D. student (Anders Wall) is supported by ARTES. Our vision is to develop an integrated tool
environment for the development of embedded real-time systems supporting each step of the development process, from design, simulation,
verification, runnable code generation, to test generation. The original plan was to to develop a code-geneartor for the UPPAAL tool. It turned out that we
had to study the problem of schedulability analysis for event-driven systems in order to generate executable code satisfying timing constrtaints specified in
the design phase.
During the first year, we have published one paper at an international conference on real time systems.
One important problem in code generation for embedded real-time systems is "schedulability analysis" that is to check whether program codes generated
can be executed or not within given deadlines. The traditional approach to schedulability analysis is often based on scheduling theory and a task model,
which has been very successful for time-driven systems, but less successful for event-driven systems.
In recent years, in the area of formal methods, there have been several advances in formal modeling and analysis of real time systems based the theory of
timed automata due to the pioneering work of Alur and Dill. Notably, a number of verification tools have been developed (e.g. Kronos and UPPAAL in the
framework of timed automata, that have been successfully applied in industrial case studies. Timed automata have proved expressive enough for many
real-life examples, in particular, for event-driven systems. The advantage with timed automata is that one may specify much relaxed timing constraints on
events (i.e. discrete transitions) than the traditional approach in which events are often considered to be periodic. However, it is not clear how the model of timed automata can be used for schedulability analysis.
Results and contributions
In this project, we plan to develop an extended version of timed automata with real-time tasks to provide a model for event-driven systems, which can be
used for modelling, schedulability analysiss, formal verification, and code generation. The main idea is to associate each discrete transition in a timed
automaton with a task (an executable program e.g. written in C or Java) with its worst case execution time. Intuitively, a discrete transition in an extended
timed automaton denotes an event releasing a task and the guard on the transition specifies all the possible arriving times of the event (instead of the
so--called minimal inter-arrival time). This yields a general model for hard real-time systems in which tasks are non-periodic. In this model, an automaton is
used to model control structuer of a systems and associated tasks are used to perform computation. Thus, code generation for such a model is reduced to
transform the automaton into a runnable program with procedure-call. However, a critical problem is to guarantee that all the tasks associated with the
automaton can be executed within their deadlines.
As the first result of this project, we have shown that the schedulability problem for the extended model can be transformed to a reachability problem for
timed automata and thus it is decidable (The result is reported in a technical report and submitted to an international conference). This result allows us to
apply model-checking tools for timed automata to schedulability analysis for event-driven systems. In addition, based on the same model of a system, we
may use the tools to verify other properties (e.g. safety and functionality) of the system. This unifies schedulability analysis and formal verification in one
framework. The next step is to study the problem of transforming such extended models into executable programs.
We believe that software tool is an efficient means for technology transfer from academy to industry. We are experiencing an increasing attention to
software tools for real-time embedded systems through our collaboration with e.g. Mecel AB, in particular tools with features for code generation. This can
also been observed in various ESPRIT projects and Swedish national research programmes and centers (e.g. ASTEC) that industrial involvements have
been growing rapidly in research activities on tool development. In e.g. the automotive industry, there is a desire for a range of tools based on formal
techniques, supporting modeling, validation, verification, executable code generation and test generation. As the project is still in the initial phase, it is still too
early to provide any applicalble results to industry. The industrial partner of this project is Mecel AB.
This is a joint project between Mälardalen Univesity and Uppsala University. The project is one of the main acticities within the development of the
UPPAAL tool developed in collaboration by Uppsala University and Aalborg University.
- Christer Ericsson, Anders Wall and Wang Yi, Timed Automata as Task Models for Event-Driven Systems, In the proceedings of RTSCA'99, IEEE press, Dec 1999. pdf.
- Henrik Thane and Anders Wall. Formal and Probabilistic Arguments for Component Reuse in Safety-Critical Real-Time Systems. ARTES Graduate Student Conference 2000.
- Wall, Anders. A Formal Approach to the Analysis of
Software Architechtures for Real Time Systems. Licenciate Thesis 2000.