# Presentation

(Created page with "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 d...") |
|||

(5 intermediate revisions by one user not shown) | |||

Line 1: | Line 1: | ||

− | The | + | <div style="width:690px; float:left;"> |

+ | The BWare project is an industrial research project that aims to provide a | ||

mechanized framework to support the automated verification of proof obligations | mechanized framework to support the automated verification of proof obligations | ||

− | coming from the development of industrial applications using the | + | coming from the development of industrial applications using the B method |

− | and requiring high guarantees of confidence. It therefore addresses Topic | + | and requiring high guarantees of confidence. It therefore addresses Topic 1 |

− | (`` | + | (``''Sécurité des systèmes numériques''<nowiki>''</nowiki>) and |

− | logiciel et du | + | Topic 2 (``''Ingénierie du logiciel et du matériel''<nowiki>''</nowiki>) |

+ | of the [http://www.agence-nationale-recherche.fr/ ANR] [http://www.agence-nationale-recherche.fr/INS-2012 ``''Ingénierie Numérique & Sécurité''<nowiki>''</nowiki>] | ||

call. | call. | ||

Line 12: | Line 14: | ||

theorem provers aims at allowing a wide panel of proof obligations to be | 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 | automatically verified by our platform. The major part of the verification tools | ||

− | used in | + | used in BWare have already been involved in some experiments, which have |

consisted in verifying proof obligations or proof rules coming from industrial | consisted in verifying proof obligations or proof rules coming from industrial | ||

applications. This therefore should be a driving factor to reduce the risks of | applications. This therefore should be a driving factor to reduce the risks of | ||

Line 18: | Line 20: | ||

verification tools to deal with a larger amount of proof obligations. | verification tools to deal with a larger amount of proof obligations. | ||

− | Beyond the multi-tool aspect of our methodology, the originality of the | + | 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 | project also resides in the requirement for the verification tools to produce | ||

proof objects, which are to be checked independently. This backend should allow | 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 | us not only to increase confidence in the produced proofs, but ultimately to | ||

− | provide interoperability between provers. The success of | + | provide interoperability between provers. The success of BWare will be |

ensured by a large collection of proof obligations provided by some of the | ensured by a large collection of proof obligations provided by some of the | ||

industrial partners of this project, which develop either tools implementing 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 | This project combines four different kinds of expertise: production of proof | ||

− | obligations for the | + | obligations for the B method; translation from set theory to first-order |

logic; automated theorem proving; proof production and proof checking. The | logic; automated theorem proving; proof production and proof checking. The | ||

− | + | BWare consortium associates academics entities ([http://cedric.cnam.fr Cedric], [http://www.lri.fr/ LRI], and | |

− | + | [http://www.inria.fr/ Inria]) and industrial partners ([http://www.mitsubishielectric-rce.eu/ Mitsubishi Electric R&D Centre Europe], [http://www.clearsy.com/ ClearSy], and | |

+ | [http://www.ocamlpro.com/ OCamlPro]). This | ||

will ensure an excellent level of expertise for the scientific aspects as well | 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 | as their exploitation for the development of software with high guarantees of | ||

Line 39: | Line 42: | ||

there is a theoretical study regarding the generation of proof obligations, as | 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 | 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 | design of a verification platform, which will gather several tools, and some | ||

extensions of these tools will be considered and developed. This platform will | extensions of these tools will be considered and developed. This platform will | ||

− | be integrated to the tool of an industrial partner ( | + | be integrated to the tool of an industrial partner ([http://www.atelierb.eu/ Atelier B] from ClearSy) |

for evaluation over industrial applications and comparison with other similar | for evaluation over industrial applications and comparison with other similar | ||

existing verification tools. An activity of interactive proof will be also | existing verification tools. An activity of interactive proof will be also | ||

Line 53: | Line 56: | ||

help to widely advertise the results of the project in different communities, | help to widely advertise the results of the project in different communities, | ||

such as academics, industrial actors, developers, and users. | such as academics, industrial actors, developers, and users. | ||

+ | </div> |

## Latest revision as of 01:54, 3 October 2012

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 ANR ``*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.