TKK / Department of Information and Computer Science / Research / Computational Logic / StMcDes
Symbolic Testing and Model Checking of Distributed Embedded Systems (StMcDes)
A research project (number 128050) funded by Academy of
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.
For software and theses see the home page of the computational logic group.
Project team members:
Latest update: 09 January 2011.