click my www
............|___
...................\
.................._|_
..................\ /
..................."
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
Calcul numérique de processus industriels
Formation, conseil, développement
Point n'est besoin d'espérer pour entreprendre, ni de réussir pour persévérer. (Guillaume le Taiseux)
Mac LAK.
___________________________________________________
Ne prenez pas la vie trop au sérieux, de toutes façons, vous n'en sortirez pas vivant.
Sources et composants Delphi sur mon site, L'antre du Lak.
Pas de question technique par MP : posez-la dans un nouveau sujet, sur le forum adéquat.
Rejoignez-nous sur : ► Serveur de fichiers [NAS] ► Le Tableau de bord projets ► Le groupe de travail ICMO
ALGORITHME (n.m.): Méthode complexe de résolution d'un problème simple.
Mac LAK.
___________________________________________________
Ne prenez pas la vie trop au sérieux, de toutes façons, vous n'en sortirez pas vivant.
Sources et composants Delphi sur mon site, L'antre du Lak.
Pas de question technique par MP : posez-la dans un nouveau sujet, sur le forum adéquat.
Rejoignez-nous sur : ► Serveur de fichiers [NAS] ► Le Tableau de bord projets ► Le groupe de travail ICMO
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.
Mac LAK.
___________________________________________________
Ne prenez pas la vie trop au sérieux, de toutes façons, vous n'en sortirez pas vivant.
Sources et composants Delphi sur mon site, L'antre du Lak.
Pas de question technique par MP : posez-la dans un nouveau sujet, sur le forum adéquat.
Rejoignez-nous sur : ► Serveur de fichiers [NAS] ► Le Tableau de bord projets ► Le groupe de travail ICMO
Envoyé par millieTout à 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.
Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
Avant de poser une question je lis les règles du forum.
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 .
" Le croquemitaine ! Aaaaaah ! Où ça ? " ©Homer Simpson
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