Specifying and Verifying Cases Retrieval System Combining Event B and Spin

This paper presents a complete study for the specification and mechanical verification of cases retrieval systems (CRS) within the generic framework that supports the many-to-many connection of formal development environments and model checkers. We aim at combining on an example, refinement techniques, verification by theorem proving and model checking in an entire development, to guarantee software correctness properties. We first build a underlying abstract system using a roles-based collaboration model, then describe a practical approach for increasingly developing flexible and reliable formal specifications of CRS using event B, exemplified on contract net protocol (CNP) as interaction contract. A proper translator is introduced as the bridge between formal specifications and model checkers. This entire development is mechanically proved with respect to safety properties using B tool and, complementally, with respect to liveness properties using the SPIN tool.