A Perfecto verification: Combining model checking with deductive analysis to verify real-life software

The paper presents an approach to the formal verification of a complete software system intended to support the flagship product of Perfecto Technologies which enforces application security over an open communication net. Based on initial experimentation, it was decided that the verification method will be based on a combination of model-checking using SPIN with deductive verification which handles the more data-intensive elements of the design. The analysis was that only such a combination can cover by formal verification all the important aspects of the complete system. In order to enable model checking of large portions of the design, we have developed an assume-guarantee approach which supports compositional verification. We describe how this general approach was implemented in the SPIN framework. Then, we explain the need to split the verification activity into the model-checking part which deals with the control issues such as concurrency or deadlocking and a deductive part which handles the data-intensive elements of the design.