ARTES
-------------------------------------------------

 
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
 

Industry contact

Lars Magnusson lars.magnusson@mecel.se
Mecel AB
Göteborg
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 Timing Constraints”

Overview

SUMMARY

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.

Research Problems

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.

Co-operation

Industrial

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.

Swedish cooperations

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.

Publications

  1. 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.
  2. Henrik Thane and Anders Wall. Formal and Probabilistic Arguments for Component Reuse in Safety-Critical Real-Time Systems. ARTES Graduate Student Conference 2000.
  3. Wall, Anders. A Formal Approach to the Analysis of Software Architechtures for Real Time Systems. Licenciate Thesis 2000.
  ---------------------line----------------------------
  Strategic Research