This research is attempting to design and implement a generic infrastructure for distributed on−the− fly verification based on models allowing functional verification of competing complex systems. This work is part of the context Construction and Analysis of Distributed Processes for the design of communication protocols and distributed systems. Whenever possible, we try to validate our proposals by developing tools, using the generic Open environment for exploration, in order to combine them with other existing tools and to allow direct interfacing with various specifications languages-these languages describe the source program to be evaluated. Applying these tools to complex, often industrial, case studies is an integral part of the process of validating the proposed methods. This systematic confrontation with implementation and experimentation problems is an essential aspect of our journey. The approach we have adopted is to address the traditional technical limitations of verifying the scaling up of programs to be audited. More precisely, we have pursued a twofold objective: i) by designing distributed algorithms containing one or more blocks of Boolean equations (with no mutually recursive inter-block dependencies), in order to increase the capacity of the resolution (currently limited there are about 108 variables on equals machines) using the computing and memory resources of a set of machines interconnected by a network. The implementation of these algorithms must have general programming interfaces that can be used by standard verification techniques and by all tools that have a connection to the Open / Caesar environment. ii) by designing and developing model-based translatable verification applications which directly benefit from the distributed resolution mechanisms proposed in the first objective. These audit tools should, as much as possible, be independent of the program description language to be verified, while having comparable performance to the best existing tools. The verification of finished state systems, whether distributed or competitive, is in practice confronted with the problem of state explosion (prohibitive size of space Vs Underlying states) that occur for realistic-sized systems that contain many parallel processes and complex data structures. Various techniques have been proposed to combat the explosion of states, such as on the fly verification and partial order reduction.
- Institution / Hochschule
- University of the Witwatersrand – Wits