Control Explicit---Data Symbolic Model Checking: An Introduction

A comprehensive verification of parallel software imposes three crucial requirements on the procedure that implements it. Apart from accepting real code as program input and temporal formulae as specification input, the verification should be exhaustive, with respect to both control and data flows. This paper is concerned with the third requirement, proposing to combine explicit model checking to handle the control with symbolic set representations to handle the data. The combination of explicit and symbolic approaches is first investigated theoretically and we report the requirements on the symbolic representation and the changes to the model checking process the combination entails. The feasibility and efficiency of the combination is demonstrated on a case study using the DVE modelling language and we report a marked improvement in scalability compared to previous solutions. The results described in this paper show the potential to meet all three requirements for automatic verification in a single procedure combining explicit model checking with symbolic set representations.