Salut!
100 % d'accord. On peut certifier qu'une certaine faille est absente, mais comme il existe une quasi-infinité de possibilités de failles, il n'est pas possible de certifier qu'on les a toutes éliminées, surtout celles qu'on ne connait pas encore.Je pense que réaliser un OS sans failles est utopique
Jean-Marc Blanc
Je pense que les preuves assistés par ordinateurs ont surtout leur intérêt pour prouver que des algorithmes fonctionnent, ce qui peut être très importants pour certains logiciels cruciaux (avions par exemple).
Cela peut aussi être intéressants pour les compilateurs même si en pratique on ne pourra jamais prouver un compilo entier avec toutes les optimisations, ...
Mais c'est vrai que pour le génie logiciel, cela a peu d'intérêt. De même pour les OS, sauf peut-être des noyau sur des systèmes embarqués vitaux.
Envoyé par millie
Tout à fait d'accord. Ces nouveaux langages pour l'assistance de preuve fonctionnent à merveille sur les petits exemples jouets. Le but des développements plus ambitieux (certification de programmes réalistes et formalisation de gros théorèmes) c'est avant tout d'identifier les obstacles au passage à l'échelle. Ceci afin de concevoir la syntaxe, les abstractions et les automatisations qui permettront à ces langages de sortir des labos pour rencontrer des usages métiers (à commencer par les maths et la sécurité des personnes).Envoyé par amaury pouly
Mine de rien on assiste à la maturation d'un nouveau paradigme.
Excellente question.Et est-ce qu'ils ont testé leurs tests ?
Dans les normes aviation DO218-ED109, il est précisé que les logiciels de tests doivent être conçus avec les mêmes niveaux de qualité que les logciels testés. Ce qui est évidement absurde, vu que les outils de tests, qui sont en pratique plus complexes que les logiciels testés, doivent être eux-mèmes testés et ainsi de suite.
Quand j'ai soulevé le problème auprès de certains des rédacteurs de la norme ED109, ils ont éludé la question, en disant que c'était de la responsabilité des dévellopeurs de s'accomoder de cette prescription.
En pratique, on peut s'arranger pour que les outils de tests soient eux aussi certifiés et testés. Par exemple on peut écrire une version préliminaire réduite dans laquelle on prouve qu'une implémentation plus complète est correcte et ainsi de suite. On peut alors réduire les risques d'erreurs à des programmes les plus simples possibles. Bien entendu, on est jamais certain qu'il ne reste pas des bugs![]()
Vous avez un bloqueur de publicités installé.
Le Club Developpez.com n'affiche que des publicités IT, discrètes et non intrusives.
Afin que nous puissions continuer à vous fournir gratuitement du contenu de qualité, merci de nous soutenir en désactivant votre bloqueur de publicités sur Developpez.com.
Partager