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.
Il n'y a rien de tel dans la norme. Elle est justement très peu technique et parle surtout de processus de fabrication. Le cpu typique est le powerPC 601 qui fait un peu d'out of order, il me semble.
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.
Projet assez génial on dirait :) Pour moi votre difficulté serait de faire valider tout le runtime qui est vendu avec ce genre de machin. Cela peut être extrêmement complexe. Le pire est le compilateur. Comment prouver que ce qui est compiler est correct, si vous n'avez pas la description de l'assembleur qui va avec ?
Pour les compilo C, on est censé prouver que le compilo génère le bon code objet. Cela a dû se faire par relecture et traçabilité entre code ASM et code C, mais maintenant, cela doit pouvoir se faire avec des exemples de code C à compiler, puis ensuite, on dit que tout code sera issue de ces blocs de base. Mais avec les trucs proprio NVIDIA, je ne vois pas comment faire ça. Vous avez regardez les "array de cpu" comme ceux de Kalray ?
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.
Mais non, je parle de formaliser la DO178, elle-même, pour inclure dans un langage toutes les étapes décrites dans la norme. Le compilateur ne ferait que vérifier la cohérence de l'ensemble des informations (type traçabilité spec<->code<->test<->couverture de test, vérification de la couverture, etc...).
Cela revient à faire un langage qui impose une spec, le teste, la traçabilité et des revues.
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Il n'y a rien de tel dans la norme. Elle est justement très peu technique et parle surtout de processus de fabrication. Le cpu typique est le powerPC 601 qui fait un peu d'out of order, il me semble.
Projet assez génial on dirait :) Pour moi votre difficulté serait de faire valider tout le runtime qui est vendu avec ce genre de machin. Cela peut être extrêmement complexe. Le pire est le compilateur. Comment prouver que ce qui est compiler est correct, si vous n'avez pas la description de l'assembleur qui va avec ?
Pour les compilo C, on est censé prouver que le compilo génère le bon code objet. Cela a dû se faire par relecture et traçabilité entre code ASM et code C, mais maintenant, cela doit pouvoir se faire avec des exemples de code C à compiler, puis ensuite, on dit que tout code sera issue de ces blocs de base. Mais avec les trucs proprio NVIDIA, je ne vois pas comment faire ça. Vous avez regardez les "array de cpu" comme ceux de Kalray ?
Mais non, je parle de formaliser la DO178, elle-même, pour inclure dans un langage toutes les étapes décrites dans la norme. Le compilateur ne ferait que vérifier la cohérence de l'ensemble des informations (type traçabilité spec<->code<->test<->couverture de test, vérification de la couverture, etc...).
Cela revient à faire un langage qui impose une spec, le teste, la traçabilité et des revues.
"La première sécurité est la liberté"