MRTC research projects

Embedded Systems Verification using Timed Automata Technology (VR)

Leader:	Paul Pettersson
Members:	Leo Hatvani, Cristina Seceleanu, Paul Pettersson
Research group:	Formal Modelling and Analysis of Embedded Systems
Status:	finished , start date: 2009-01-01 , End date: 2011-12-31
Funding:	Swedish Research Council (VR)

Overview

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.

Latest project publications [ Show all publications ]

Modeling and Analysis of Adaptive Embedded Systems using Adaptive Task Automata, Leo Hatvani, Cristina Seceleanu, Paul Pettersson, 4th Workshop on Adaptive and Reconfigurable Embedded Systems, April, 2012

Adaptive Task Automata: A Framework for Verifying Adaptive Embedded Systems, Leo Hatvani, Paul Pettersson, Cristina Seceleanu, FASE'12: Proceedings of the 15th International Conference on Fundamental Approaches to Software Engineering, p 115-129, Springer-Verlag Berlin Heidelberg, Editor(s):Juan de Lara and Andrea Zisman, March, 2012

A Formal Analysis Framework for AADL, Stefan Björnander, Cristina Seceleanu, Kristina Lundqvist, Paul Pettersson, The Journal of Science and Technology, November, 2011

Mälardalen University |
Box 883 |
721 23 Västerås/Eskilstuna |
021-101300, 016-153600 |
webmaster |
Latest update: 2012.08.24