A mechanically proved development combining B abstract systems and Spin

We present a complete study involving in the one hand refinement and an associated theorem proving tool and, on the other hand liveness verification with an associated tool. The event B method is used in the first part whereas Spin is used in the second one. The Spin validation tool is used to simulate and check B abstract systems. This entire development is mechanically proved with respect to safety properties using B tool and with respect to liveness properties using the Spin tool. The semantic compatibility between Spin processes and B systems is used as a basis for the translation from one framework to the other. We show through this study that for some B systems, the Spin tool is well adapted for complementary analysis. The study combines on an example of concurrent system, refinement techniques, verification by theorem proving and model checking.