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 modelchecking 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.