Heuristic Support for Model Checking of Asynchronous Systems

OData support
Supervisor:
Vörös András
Department of Measurement and Information Systems

Nowadays, hardware and software systems require a high degree of assurance of design correctness. However, these systems have reached such a complexity that IT professionals are no longer able to handle the whole lifecycle of the product without support. The verification of these systems is often based on formal methods, and especially on model checking, which is a widely used approach to investigate the behaviour of discrete state models. State-space generation is an essential prerequisite to verify the requirements against the system. Nevertheless the exhaustive generation of complex systems’ state-spaces is extremely hard because of the time and storage requirements. The state space explosion phenomenon describes this behavior: as the complexity of a system increases, the memory and time required to store the combinatorically expanding state space can easily become excessive.

According to the newest experimental results, the saturation algorithm can be efficiently used to overcome the limitations of memory and time requirements. Nevertheless, most of today’s hardware are built with multi-core processors so the need for parallel algorithms is growing to utilize the additional resources and to shorten the runtime length of the state-space generation. Formerly, we made a Scientific Students’ Association Report which investigates the parallelization of the saturation algorithm. The main aspects of the parallel algorithm are described in this paper too.

Beyond parallel algorithm heuristics based model checkers are used to shorten the time required to investigate the behavior of the system. As part of my work I developed a herustics based algorithm for transition pre-firing. The motivation of the algorithm was given by the results of the parallel saturation algorithm’s profiling, which carried out that in certain scenarios not all of the computational resources were exploited during the state space generation. One may manage to utilize these additional resources to pre-generate parts of the system’s state space, so that it will be useful for the saturation algorithm and reach further performance improvement. However, the applied heuristics have an important role as it is a nontrivial task to find the useful parts.

In this paper I experimented several heuristics, measured and compared their efficiency based on statistics. I integrated the pre-firing modul into the PetriDotNet framework developed at the Department of Measurement and Information Systems. As part of my work I compared the runtime length of the formerly implemented sequential and parallel algorithms against the one that exploits pre-firing too, with the use of several real-world systems’ models. The experimental results showed that I managed to achieve additional speedups in the generation of several models’ state space. In some cases the sequential algorithm was faster than the parallel one, but with the addition of pre-firing in the parallel saturation there wasn’t significant difference in the runtime length anymore.

Downloads

Please sign in to download the files of this thesis.