Embedded Systems Verification using Timed Automata Technology (VR)

Division:

Division of Networked and Embedded Systems

Research Group:

Formal Modelling and Analysis of Embedded Systems

Status:

finished

Start date:

2009-01-01

End date:

2011-12-31

The main motivation of this project is the need for design techniques to support the development of software in embedded systems. In such systems, the software is embedded into a hardware product, and must operate correctly with respect to timing constraints, while using limited resources, such as CPU, energy, memory, bus bandwidth, etc. Hence, an important concern during the design of such systems is to predict that the limited resources of the target platform will not be exceeded. Automated mathematical techniques that would guarantee all of the previously mentioned behviours, starting from early design stages, are still missing. This project will focus on research in this problem area, with the goal to develop formal description techniques for embedded systems based on automata theoretic approaches, supporting the early development life-cycle phases with prediction analysis techniques for abstract design descriptions. The following will be the main research directions of the project:

  • -an automata theoretic approach based on combining the models of priced timed automata and task automata to develop a formal modeling framework for function, timing, and resources in embedded system applications
  • -algorithmic techniques for verification of functional, timing, and resource consumption of embedded systems, and
  • -a tool for automatic verification of the proposed model, based on the existing tools Times and Uppaal.

Paul Pettersson, Professor

Email: paul.pettersson@mdu.se
Room:
Phone: +46-739-607382

Apr 2014
Innovationer för Framtidens hälsa