Symbolic Model Checking Visualization

Abstract

The industrial deployment of formal verification technology that has not yet reached its maturity is extremely difficult. The more automated and therefore most widely used formal verification technology, symbolic model checking, has a severe problem of limited capacity. The capacity limitation reflects itself in long, and most importantly, unpredictable run time duration which results in low productivity.

In this paper, we demonstrate how we integrated techniques from the fields of algorithm animation, performance monitoring, and knowledge engineering in order to boost two major problem areas of model checking: the capacity limitation and low productivity. We have developed a prototype, called Palette, in order to demonstrate these concepts.

Palette uses visualization techniques to give insight to the execution of the symbolic model checking algorithms. Furthermore, it tracks the progress of the verification run and enables mid-course analysis of the status. Palette makes a step forward in estimation of the run time duration by predicting the amount of work done in some selected execution tasks, and informing the ones that are to be executed in the future. An additional important goal of Palette is to assist in building and automating the model checking usage methodology, and consequently to reduce the need for user expertise and intervention. In this aspect, Palette is a light-weight expert system for model checking. It can determine which algorithms are not efficient and reason on their failure. It can also advice on how to make a verification task complete successfully.