A Proof-Based Mechanized Plate-Forme for the Verification of B Proof Obligations – BWare

The BWare project is an industrial research project that aims to provide a mechanized framework to support the automated verification of proof obligations coming from the development of industrial applications using the B method and requiring high guarantees of confidence. It therefore addresses Topic 1 (``Sécurité des systèmes numériques'') and Topic 2 (``Ingénierie du logiciel et du matériel'') of the ``Ingénierie Numérique & Sécurité'' call.

The methodology used in this project will consist in building a generic platform of verification relying on different theorem provers, such as first-order provers and SMT (Satisfiability Modulo Theories) solvers. The variety of these theorem provers aims at allowing a wide panel of proof obligations to be automatically verified by our platform. The major part of the verification tools used in BWare have already been involved in some experiments, which have consisted in verifying proof obligations or proof rules coming from industrial applications. This therefore should be a driving factor to reduce the risks of the project, which can then focus on the design of several extensions of the verification tools to deal with a larger amount of proof obligations.

Beyond the multi-tool aspect of our methodology, the originality of the BWare project also resides in the requirement for the verification tools to produce proof objects, which are to be checked independently. This backend should allow us not only to increase confidence in the produced proofs, but ultimately to provide interoperability between provers. The success of BWare will be ensured by a large collection of proof obligations provided by some of the industrial partners of this project, which develop either tools implementing the B method or applications involving the use of the B method.

This project combines four different kinds of expertise: production of proof obligations for the B method; translation from set theory to first-order logic; automated theorem proving; proof production and proof checking. The BWare consortium associates academics entities (CEDRIC, LRI, and Inria) and industrial partners (Mitsubishi Electric R&D Centre Europe, ClearSy, and OCamlPro). This will ensure an excellent level of expertise for the scientific aspects as well as their exploitation for the development of software with high guarantees of confidence required by today applications.

The organization of the project consists of several parts. Among these parts, there is a theoretical study regarding the generation of proof obligations, as well as the formalization of several models for the set theory underlying the B method. This part is intended to support another part concerning the design of a verification platform, which will gather several tools, and some extensions of these tools will be considered and developed. This platform will be integrated to the tool of an industrial partner (Atelier B from ClearSy) for evaluation over industrial applications and comparison with other similar existing verification tools. An activity of interactive proof will be also conducted in order to optimally combine the automated provers, and some optimizations of the verification tools will be studied as well.

The dissemination of the results will be ensured by a web site, publications, organization of seminars (and possibly workshops), and free availability of the verification platform. The various natures of the members of the consortium will help to widely advertise the results of the project in different communities, such as academics, industrial actors, developers, and users.