Methods for provably correct design of embedded systems

Our research goal is elaboration of formal theories, methods and tools for embedded distributed systems design with special focus on scheduling, verification, model based testing and code generation.

Domain specific features studied in this research are dependability particularly fault tolerance, nonlinear and hybrid dynamics, safety criticality, real time constraints, autonomous behavior, and reconfigurability.

Theoretical basis comprises real time temporal logic and hybrid automata, specially variations of timed automata. Design process is considered as a sequence of model transformations where abstraction and refinement transformations enhance systematic construction of specifications and models, needed for automatic design synthesis and verification steps.

The application domain includes mission critical and human adaptive robotics, robotic manufacturing systems, and multi-robot systems.

Members of the working group:

Name Position Degree
Jüri Vain senior researcher PhD