Presentation

From BWare
Jump to: navigation, search
 
Line 1: Line 1:
 +
<div style="width:690px; float:left;">
 
The BWare project is an industrial research project that aims to provide a
 
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 B method
 
coming from the development of industrial applications using the B method
 
and requiring high guarantees of confidence. It therefore addresses Topic 1
 
and requiring high guarantees of confidence. It therefore addresses Topic 1
(<nowiki>``Sécurité des systèmes numériques''</nowiki>) and Topic 2 (``Ingénierie du
+
(``''Sécurité des systèmes numériques''<nowiki>''</nowiki>) and
logiciel et du matériel'') of the ``Ingénierie Numérique & Sécurité''
+
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 30: Line 32:
 
obligations for the B method; translation from set theory to first-order
 
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 (Cedric, Lri, and
+
BWare consortium associates academics entities ([http://cedric.cnam.fr Cedric], [http://www.lri.fr/ LRI], and
Inria) and industrial partners (Mitsubishi Electric R&D Centre Europe, ClearSy, and OCamlPro). This
+
[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 42: Line 45:
 
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 (Atelier B from ClearSy)
+
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

Personal tools
Namespaces

Variants
Actions
Navigation
Toolbox