Pour info, j'ai fais uniquement du DAL A (code qui vole, générateur de donné, outils de validation). 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é.
SCADE est souvent utilisé dans les fadec, mais il n'y a aucune "preuve". Le langage est formel dans le sens ou il ne comporte pas d’ambigüité. Et le compilo est certifié.
D'ailleurs pour les DAL >= C, il devient difficile d'employer des CPU multi-cœurs ou avec un GPU moderne tellement que c'est contraignant vis à vis des normes.
Cela commence tout doucement. La première version de vxworks multicpu, tournait avec 2 instances d'OS, comme si il y avait 2 ordinateurs. C'est très compliqué de calculer le temps d’exécution avec ce genre de machine (ex: il y a une perte de perf de 20% sur les 2 cpu à cause de l'usage du bus mémoire). Si tu prends des marges de fou, avoir 2 cpu n'a plus trop d’intérêt.
Mais la mode IMA, c'est de tout "virtualiser" plus ou moins statiquement. Leur rêve est d'avoir des racks standards et de mettre les applications sur les ordinateurs fonctionnelles.
Concernant les GPU, je n'ai pas encore vu de code certifié. En graphique, il utilise de l'openGL SC, genre d'opengl 1.0, je crois que la dernières version a simplement pris l'api opengl ES vu comme plus propre. Il n'y a pas de shader la-dedans (il faudrait qualifier le compilateur...).
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é. Mais cela va au-delà du code pure, car il faut gérer la documentation (les revues de code humaine, les descriptions api, le rapport d'architecture), les versions, les tests (et leur couverture), la traçabilitée.
[^] # 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.
Pour info, j'ai fais uniquement du DAL A (code qui vole, générateur de donné, outils de validation). 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é.
SCADE est souvent utilisé dans les fadec, mais il n'y a aucune "preuve". Le langage est formel dans le sens ou il ne comporte pas d’ambigüité. Et le compilo est certifié.
Cela commence tout doucement. La première version de vxworks multicpu, tournait avec 2 instances d'OS, comme si il y avait 2 ordinateurs. C'est très compliqué de calculer le temps d’exécution avec ce genre de machine (ex: il y a une perte de perf de 20% sur les 2 cpu à cause de l'usage du bus mémoire). Si tu prends des marges de fou, avoir 2 cpu n'a plus trop d’intérêt.
Mais la mode IMA, c'est de tout "virtualiser" plus ou moins statiquement. Leur rêve est d'avoir des racks standards et de mettre les applications sur les ordinateurs fonctionnelles.
Concernant les GPU, je n'ai pas encore vu de code certifié. En graphique, il utilise de l'openGL SC, genre d'opengl 1.0, je crois que la dernières version a simplement pris l'api opengl ES vu comme plus propre. Il n'y a pas de shader la-dedans (il faudrait qualifier le compilateur...).
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é. Mais cela va au-delà du code pure, car il faut gérer la documentation (les revues de code humaine, les descriptions api, le rapport d'architecture), les versions, les tests (et leur couverture), la traçabilitée.
"La première sécurité est la liberté"