Le KVB qui contrôle la vitesse des TGV est développé en B. Des gestions d'aiguillages d'Alstom sont développés en B. etc.
Le ferroviaire aime bien le formel avec des produits de http://www.absint.com/ . Mais ils s'agit souvent de prouver "des théorèmes" et non des "spec complètes".
Assertion un peu gratuite. Le standard DO-178C permet justement d'utiliser des méthodes formelles pour remplacer des tests, ce que la version précédente (178B) ne permettait pas. Et il y a aussi le DO-333 ("Formal Methods Supplement to DO-178C and DO-278A").
Airbus est un gros consommateur de méthodes et outils formels : CAVEAT, FLUCTUAT, Astrée, SCADE, CompCert, Frama-C, ...
[^] # Re: On verra
Posté par David Mentré (site web personnel) . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 1.
:-) Pas mal oui : http://www.clearsy.com/wp-content/uploads/carte-monde-b-fr.jpg
Le KVB qui contrôle la vitesse des TGV est développé en B. Des gestions d'aiguillages d'Alstom sont développés en B. etc.
Tu peux jeter un œil sur le travail fait par ClearSy pour le CBTC de Thales sur la Flushing Line de New York. Le but est bien de prouver des propriétés système (i.e. dans une spec complète).
http://www.tools.clearsy.com/resources/formal-proofs-for-the-nyct-line-7-modernization-project/
Assertion un peu gratuite. Le standard DO-178C permet justement d'utiliser des méthodes formelles pour remplacer des tests, ce que la version précédente (178B) ne permettait pas. Et il y a aussi le DO-333 ("Formal Methods Supplement to DO-178C and DO-278A").
Airbus est un gros consommateur de méthodes et outils formels : CAVEAT, FLUCTUAT, Astrée, SCADE, CompCert, Frama-C, ...