Skip to main content.

Why DiVinE ?

The computing power of computers has increased by a factor of a million over the past couple of decades. As a matter of fact, the development effort, both in industry and in academia, has gone into developing bigger, more powerful and more complex applications. In the next few decades we may still expect a similar rate of growth, due to various factors such as continuing miniaturization, parallel and distributed computing.

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.

A lot of attention has been paid to the development of approaches to battle the state space explosion problem. Many techniques, such as abstraction, state compression, state space reduction, symbolic state representation, etc., are used to reduce the size of the problem to be handled allowing thus a single old-fashioned single-processor computer to process larger systems. All these methods can be therefore characterized as reduction techniques.

Verification and analysis methods that are tailored to exploit the capabilities of the new hardware architectures are slowly appearing as well. These platform-dependent techniques focus on increasing the amount of available computational power. These are, for example, techniques to fight memory limits with efficient utilisation of external I/O devices, techniques that introduce cluster-based algorithms to employ aggregate power of network-interconnected computers, or techniques to speed-up the verification on multi-core processors.

The idea of exploiting hard disks or parallel computers in verification already appeared in the very early years of the formal verification era. However, inaccessibility of cheap parallel computers with sufficiently fast external memory together with negative theoretical complexity results excluded these approaches from the main stream in formal verification. The situation changed dramatically during the past several years. The computer progress over the past two decades has measured several orders of magnitude with respect to various physical parameters such as computing power, memory size at all hierarchy levels from caches to disk, power consumption, physical size and cost. In particular, the focus of novel computer architectures in parallel and distributed computing has shifted away from unique massively parallel systems competing for world records towards smaller and more cost effective systems built from personal computer parts. In addition, recent shift in the emphasis of research on parallel algorithms to pragmatic issues has provided practically efficient algorithms for solving computationally hard problems. As a matter of fact, interest in platform-depended verification has been revived and DiVinE was born.

About DiVinE

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).

LTL model checking algorithms in DiVinE follow the automata-based approach. Algorithms find accepting cycles in the product of the system model and a Buchi automaton for the negation of the formula.

In most sequential LTL model checkers Nested Depth-First Search and Tarjan's decomposition into strongly connected components are used for accepting cycle detection. Unfortunately, both algorithms strongly rely on depth-first search postorder which computation is known to be inherently sequential. Therefore, these algorithms are unsuitable for being used in parallel setting. DiVinE implements new algorithms for parallel accepting cycle detection problem. These are briefly described on the respective tool pages.

DiVinE Tools and Branches

DiVinE tools differ in the platforms they are supposed to be run on, while DiVinE branches are domain specific tools.

DiVinE BRANCHES
DiVinE TOOLS Concurrent Systems Probabilistic Systems Biological Systems
Clusters (distributed-memory) DiVinE CLUSTER
is a parallel distributed-memory enumerative model-checking tool for verification of concurrent systems. The tool can employ aggregate power of network-interconnected workstations to verify systems whose verification is beyond capabilities of sequential tools. As a standard model-checker, DiVinE Cluster can be used to prove correctness of verification models as well as to detect early design errors.
ProbDiVinE
is an enumerative model-checking tool for verification of probabilistic systems represented as Markov decision processes. The tool supports qualitative LTL model-checking of MDPs and is supposed to be run on clusters of workstations.
BioDiVinE (under development)
is a tool for exploring dicrete models of biological systems, predicting outcomes of experiments, and verifying specific properties at the model, based on techniques for scalable qualitative simulation and analyzis of integrated regulatory networks dymamics.
Multi-cores (shared-memory) DiVinE MULTI-CORE
is a parallel shared-memory enumerative model-checking tool for verification of concurrent systems. The tool can employ full power of modern 64-bit multi-core architectures. Similarly to DiVinE Cluster, it can be used to prove correctness of verification models as well as to detect early design errors.
ProbDiVinE MC is an enumerative shared-memory model-checking tool for verification of probabilistic systems represented as Markov decision processes. The tool supports both qualitative as well as quantitative approaches to LTL model-checking of MDPs.
GPUs DiVinE CUDA
is an open source standalone verification tool that supplements DiVinE verification tool chain with GPU accelerated LTL model checking of concurrent systems. DiVinE CUDA builds upon the MAP algorithm reformulated in terms of repeated matrix-vector product. The tool first generates state space of the model under inspection, stores it in the form of a matrix, and then it employs CUDA architecture to solve the accepting cycle detection problem on the graph represented with the matrix.
Hard Disks DiVinE I-O (under development)
is a distributed-memory enumerative model-checking tool for verification of concurrent systems on external memory devices. The tool implements I/O efficient LTL model-checking algorithms, where the goal is to reduce the number of expensive I/O. This is because the access to information stored on an external device is orders of magnitude slower than the access to information stored in main memory. It can be used both to prove correctness of verification models as well as to detect early design errors.