Symbolic Testing and Model Checking of Distributed Embedded Systems (StMcDes)

A research project (number 128050) funded by Academy of Finland
Jan 1, 2009 - Dec 31, 2012

Project leader: Prof. Ilkka Niemelä

Research Personnel: Keijo Heljanko, Tommi Junttila, Jori Dubrovin, Roland Kindermann, Kari Kähkönen

Summary: This project focuses on basic research in the area of testing and model checking methods for distributed embedded systems. The main challenge we want to tackle is the theory behind efficient software development, especially validation, methods for embedded systems. In particular, we are interested in distributed embedded systems composed of software components with clearly defined behavioral interfaces. Examples of the application domain include distributed sensor networks, distributed automation systems, instrumentation and control systems, software systems in cars, and data-communications protocols in embedded devices.

The research focuses on validating distributed embedded software systems with several basic research topics building on the following methods: (i) unfoldings, (ii) concolic testing, (iii) methods for behavioral interface specifications, (iv) use of SAT and SMT solvers, and (v) symbolic techniques for analyzing timed aspects of distributed systems. Our aim is to significantly extend the state of the art, especially in the theory of validation methods for distributed embedded software. A long term goal is to enable source code level validation of such software systems.

The project builds on extensive previous work of the research group on symbolic model checking using propositional satisfiability (SAT) solvers and on partial order methods for concurrency.

Publications of the project

For software and theses see the home page of the computational logic group.

Local Information

• Remember to acknowledge the financial support from the Academy of Finland using the project number 128050.
• Remember to add you publications to the bibdb system and use the flag StMcDes in the publications related to this project.