Department of Distributed and Dependable Systems

Building at Mala Strana

The Department of Distributed and Dependable System is responsible for research and education in the advanced techniques for building reliable component-based software especially in the field of distributed and dependable systems, spanning from smart cyber-physical systems and IoT to cloud-based backends. Our research comprises advanced software architectures, adaptation, model-driven development, model-based testing, formal verification techniques, performance measurement and modeling, and other fields.

The vision pursued by our department is that of high-quality scientific research with strong industrial relevance, with the aim to enable rapid and cost-efficient production of complex and reliable software systems. To achieve this vision, our department actively collaborates on the national and international level with both academic and industrial partners. Recent projects include Multi-Paradigm Modelling for Cyber-Physical Systems (COST), ASCENS (FP7 FET IP), RELATE (FP7 ITN), Q-ImPrESS (FP7 STREP).

Research Topics

Smart Cyber-Physical Systems and IoT

We focus on state-of-the-art methods of model-driven development, requirements-oriented design, and component-based modeling and development. We specifically target large-scale software-intensive cyber-physical systems and aim at developing holistic, multi-paradigm, and well-integrated methods for modeling and developing such systems. This research primarily takes place in the scope of DEECo and IRM projects.

Automated Verification of Software

We develop techniques and tools for automated verification of programs that use multiple threads and data containers. A special focus is given to incremental and modular approaches to verification. Most of our techniques are based on predicate abstraction, Craig interpolants, static analysis, and symbolic execution.

Performance Modeling

Performance modeling has many applications in understanding and estimating system performance. We focus on analyzing the effects of sharing low level system resources, such as the processor cores or the memory architecture.

Model-based Testing

In model-based testing, formal specifications are used for testing purposes. In our work, we consider different formal notations: Abstract State Machines, feature models, combinatorial models, NuSMV models, and Boolean expressions. The first field of our research consists in devising abstraction and decomposition techniques for test case generation using model checker and a SAT/SMT solver. Another field of research consists in evaluating the quality of the specifications, and proposing ways to automatically repair them. The third field of research consists in checking that the implementation really reflects its specification by offline testing or runtime verification.

For Students

The teaching activities of our department rely strongly on personal collaboration with individual students. We involve bachelor and master students in our research through various types of individual and group projects. See the detailed description of our projects. This helps students in their future careers by providing a technically demanding experience that exercises the ability to formulate ideas and to apply critical reasoning. The results of the work on the project can, of course, be used as bachelor/master theses. If you are interested in Ph.D. studies, please see our dedicated page about doctoral studies.

Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>
  • How to find us?
Modified on 2017-08-16