Abstract

Automated verification of practical systems is computationally very hard. One of possibilities to verify extensive systems is to use the accumulated power of computer clusters. Recently, many distributed algorithms for model checking have been developed. The objectives of the DIVINE project are to create an environment for development of distributed algorithms and simultaneously to provide a set of distributed algorithms in the form of a verification tool. The aims of the Master thesis are to design a modeling language for DIVINE and to implement its interpreter. The thesis also involves development of the main modules of the tool in collaboration with other members of the development team. The work on the thesis also comprises the building of publicly available software package including a basic documentation. The other aims of the thesis include researching possible directions of future development of the tool and initial study of implementation of such extensions. …víceméně