Les démonstrations formelles ne sont pas accepté, en DO178b, et commence à l'être en DO178c. Le problème principale est que l'outil de validation lui-même doit être écris en DAL A pour être accepté.
Je suis au courant de cela, je disais juste que des équipes se servent de cela durant les étapes de développement pour gagner du temps dans la période avant la certification et éviter de devoir y passer plusieurs fois (car c'est cher).
Je sais bien que ces résultats ne sont pas exploités par les agences de certification ou de contrôle.
Cela commence tout doucement.
Oui, c'est bien ce que je dis, la migration est lente. Si je me souviens bien, un CPU dans la norme DO est considéré comme valide sans plus de preuves que cela s'il est monocoeur et ne réorganise pas l'ordre des instructions... Ce qui est de plus en plus rare aujourd'hui.
Concernant les GPU, je n'ai pas encore vu de code certifié.
Le problème du GPU c'est aussi qu'ils partent sur des hypothèses de GPU simples et donc assez peu puissants. Typiquement on a tâté les limites de la DO avec du Tegra K1 en DAL C, avec donc un CPU et un GPU qui ont une grande mémoire partagée, qui sont très modernes (donc réorganisation des instructions par exemple) et très parallélisés.
Ce cas de figure n'est pas vraiment documenté dans les standards aéro, et ils ont globalement 20 ans de retard sur ce qui est considéré comme standard. Ce qui est un soucis pour introduire bien sûr des calculs plus puissants pour le contrôle de l'appareil.
A part ça, je suis persuadé qu'il doit être possible de pouvoir créer un langage qui respecte toutes les contraintes de la DO178b, de le bootstraper et ensuite de pouvoir écrire plus facilement des applications qualifié.
Je n'en suis pas sûr, quand je m'y étais un peu intéressé il semblait impossible de pouvoir (mathématiquement) faire le langage parfait qui puisse exprimer n'importe quel programme de manière assez simple et en garantir la preuve de son bon fonctionnement.
Car bon, si pour réaliser un noyau de la taille de Linux ou Windows, prouvé fonctionnel, il faut des années de travail, avec une maintenance difficile et des fonctionnalités en moins, ça risque d'être difficile à imposer.
[^] # Re: Le cerveau n'est pas logique
Posté par Renault (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Je suis au courant de cela, je disais juste que des équipes se servent de cela durant les étapes de développement pour gagner du temps dans la période avant la certification et éviter de devoir y passer plusieurs fois (car c'est cher).
Je sais bien que ces résultats ne sont pas exploités par les agences de certification ou de contrôle.
Oui, c'est bien ce que je dis, la migration est lente. Si je me souviens bien, un CPU dans la norme DO est considéré comme valide sans plus de preuves que cela s'il est monocoeur et ne réorganise pas l'ordre des instructions... Ce qui est de plus en plus rare aujourd'hui.
Le problème du GPU c'est aussi qu'ils partent sur des hypothèses de GPU simples et donc assez peu puissants. Typiquement on a tâté les limites de la DO avec du Tegra K1 en DAL C, avec donc un CPU et un GPU qui ont une grande mémoire partagée, qui sont très modernes (donc réorganisation des instructions par exemple) et très parallélisés.
Ce cas de figure n'est pas vraiment documenté dans les standards aéro, et ils ont globalement 20 ans de retard sur ce qui est considéré comme standard. Ce qui est un soucis pour introduire bien sûr des calculs plus puissants pour le contrôle de l'appareil.
Je n'en suis pas sûr, quand je m'y étais un peu intéressé il semblait impossible de pouvoir (mathématiquement) faire le langage parfait qui puisse exprimer n'importe quel programme de manière assez simple et en garantir la preuve de son bon fonctionnement.
Car bon, si pour réaliser un noyau de la taille de Linux ou Windows, prouvé fonctionnel, il faut des années de travail, avec une maintenance difficile et des fonctionnalités en moins, ça risque d'être difficile à imposer.