Formal verification and analysis

With the increase in complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality and reliability. Various techniques for automated and semi-automated analysis and verification have been successfully applied to real-life computer systems. However, these techniques are computationally demanding and memory-intensive in general and their applicability to extremely large and complex systems routinely seen in practice these days is limited. The major hampering factor is the state space explosion problem due to which large industrial models cannot be efficiently handled unless we use more sophisticated and scalable methods and a balance of the usual trade-off between run-time, memory requirements, and precision of a method.

Our goal is to attack the scalability problem by exploiting the capabilities of modern hardware architectures. We are developing methods and techniques that fight memory limits with efficient utilisation of external I/O devices, introduce cluster-based algorithms to employ aggregate power of network-interconnected computers, speed-up the verification on multi-core processors or accelerate verification using GPU devices.


Main research priorities

  • Parallel verification and analysis. The goal is to develop parallel and distributed algorithms and their experimental comparison. The emphasis is on parallel model-checking of finite-state systems and on model-checking of probabilistic and hybrid systems.
  • Verification on external disks. I/O-efficient algorithms were introduced for computational problems involving manipulation of massive amounts of data. In the area of I/O-efficient algorithms the main goal is exactly to develop algorithms that minimize the number of block transfers (I/Os) used to solve a given problem. Given the context of formal verification, we explore possibilities of applying I/O efficient techniques to (distributed) model checking algorithms. We are particularly interested in I/O efficient algorithms for cycle detection and accepting cycle detection problems that are the core algorithmic problems to be solved in most practical model checking approaches.
  • DiVinE verification tool. DiVinE is an open source and extensible system for platform-dependent formal verification of computer systems. DiVinE is in fact a set of tools each of them tailored to a particular platform, like distributed-memory (DiVinE Cluster), shared-memory (DiVinE Multi-Core), external hard disks (DiVinE I-O) etc. DiVinE in its current development phase offers mainly tools for platform-depended model checking of finite state systems against specification formulated in linear temporal logics (LTL). Special DiVinE branches focus on model-checking of probabilistic systems (Markov decision processes) - ProbDiVinE and on analyzis of complex biological systems BioDiVinE (under development).

Research team

The research is performed in the Laboratory for Parallel and Distributed Systems ParaDiSe. The web pages of the laboratory give more detailed and complete picture about our research related activities, including publications, seminars, research projects etc.


Contact

kontakt
prof. Luboš Brim
Telefon: +420-549 49 3647
Email: brim(at)fi.muni.cz
http://www.fi.muni.cz/usr/brim/
http://paradise.fi.muni.cz/