Discussion :

[Garulfo]

C'est un métro qui fonctionne sans conducteur.
Des systèmes de preves formelles ont été utilisés pour valider le système.
Les traces que j'en ai retrouvé parlent d'ASA+ et de B (que je confond allègrement avec Z).
- W

Il y a beaucoup de chose sur Meteor.
Entre autre du C++ et de l'ADA. La partie à risque a été spécifiée en B (condition imposée par la RATP à Matra) puis raffinée jusqu'à du code ADA.
IL y a eu au moins quatre OS mis en jeu, la partie sécuritaire étant sur SunOS (il faut des bons outils pour faire du bon travail )

Il y a eu des bugs sur Meteor... mais pas sur la partie spécifiée en ADA. Il y a eu quasiment 0 retour atelier après les tests d'acceptation (sur site donc) pour la partie critique.

Mais la "sécurité" ne s'est pas arrêté là. Il y a un système de protection supplémentaire, juste au cas où, une mutation de code arrive... on est parano dans ce genre de partie logicielle. Mais il y a une raison à ca... et un coût associé.

Quoiqu'il en soit Meteor est une vraie réussite.

[Garulfo]

...
Pour la ligne 14, ils ont du payer encore bien plus pour un code "simple". mais ils avaient une exigence de qualité encore bien plus grande. De ce que j'ai lu dans les posts précédents, la validation a du couter bien plus cher que le code lui-même(vu le contexte, ça me parait justifier). Mais aux yeux des décideurs financiers, peu d'applications méritent un budget de validation à la hauteur du budget de réalisation - d'ou le nombre de bugs constatés dans certaines applis(vous avez dit jeu PC ?)

Et ces décideurs ont souvent tort. Beaucoup d'argent est parti sur la validation de Meteor, la formation des ingénieurs à B et la preuve des raffinements. En revanche avec un 0-retour atelier, l'investissement a été tellement rentable que Matra a utilisé sa méthode même quand ce n'était pas imposé par le client. À proprement parler, le code de la partie sécuritaire a coûté 0$ puisqu'entièrement généré.

Ca montre que l'investissement a priori est plus rentable en moyenne, surtout sur ce genre de projet (bien sûr). Je suis intimement convaincu que ce sera la manière de faire dans un avenir relativement éloigné (20/30 ans?)

[Garulfo]

100% d'accord avec Garulfo (ça t'étonnes ? )

Ca devient lassant... il faudrait qu'on change ca

[Donaldo]

Garulfo ouah je suis impressionné sur toute l'information que tu as sur meteor (ligne 14), tu as piqué des infos directements à la ratp? mdr

[Garulfo]

Garulfo ouah je suis impressionné sur toute l'information que tu as sur meteor (ligne 14), tu as piqué des infos directements à la ratp? mdr

J'ai travaillé là-bas dans l'équipe de support et de recherche. Ça aide pour les infos. Mon mémoire de DEA est sur la preuve automatisé dans l'Atelier B à Matra. Plus généralement, je suis chercheur en génie logiciel et dans les méthodes formelles spécifiquement.

[Donaldo]

Je comprends mieux.
J'ai fais de la theorie des langages formels, ah la la comment je n'ai pas aimé lol.
Avec des automates de partout tu ne sais même pas a quoi ça sert concrètement.
Ton truc il fait ça ah ok tant mieux pour toi mdr.

En tout cas comme quoi il y avait une finalité dans la matière, j'aurais pus bosser pour meteor

[HanLee]

Mais les langages formels, ça n'a rien à voir !
Même si ça peut servir pour les méthodes formelles.

Ce que t'as fait avec les automates, c'est la théorie des langages de programmation, les grammaires et tout!

Puis si, ça sert concrètement pour faire des compilateurs ou interpréteurs (lex/yacc...)...

[Garulfo]

Mais les langages formels, ça n'a rien à voir !
[...]

Enfin exagère pas... il y a beaucoup de langage formel dans les méthodes formels. Mais effectivement il y a une certaine erreur d'interprétation de Donaldo je pense.

[Donaldo]

Je vois donc je connais pas les méthodes formels.

[souviron34]

Ca devient lassant... il faudrait qu'on change ca

pas de problèmes

Il y a eu des bugs sur Meteor... mais pas sur la partie spécifiée en ADA. Il y a eu quasiment 0 retour atelier après les tests d'acceptation (sur site donc) pour la partie critique.
.

Tout est dans le "quasiment"

ça n'est pas zéro...

Donc, on en revient à l"origine du débat.

Zéro bug ça n'existe pas.

On peut s'en approcher, prendre tout un tas de protections, etc etc etc...

Mais il y a toujours une possibilité

[wiztricks]

Il est clair que 0 bugs est difficile à atteindre et nous n'ignorons pas des catastrophes comme la fusée Ariane ou autres déboires.

Ce qui me semble important de souligner dans cette discussion, c'est qu'on ne construit pas ce genre de solution de la même façon que les logiciels que nous avons l'habitude de développer.

Cela a une incidence sur les coûts (dissuasive pour le projet commun), sur les méthodologies, sur les gens (qui doivent les appliquer de façon rigoureuse), sur le cycle de vie (la gestion du changement est particulièrement délicate), et aussi sur les technologies retenues (il n'est pas nécessaire que cela soit plus cher, il faut aussi rester "simple").

- W

[Garulfo]

[...]
Tout est dans le "quasiment"
ça n'est pas zéro...
Donc, on en revient à l"origine du débat.
Zéro bug ça n'existe pas.[...]

Tout à fait... c'était effectivement un point important de mon message.

[Donaldo]

He bien j'ai compris bien assez tôt que le zéro bug n'existait pas, et on est parti par la suite comment allé vers le zéro bug.
Et j'ai trouvé les explications intéressantes, donc n'arrêtons pas l'échange de connaissance, car celui-ci a pour question maintenant, quelles sont les méthodes pour arriver le mieux possible au 0 bug.
Donc si d'autres veulent partager leurs connaissances allez y.