<publireportage>
Effectivement, certaines morceaux du code emarqué critique dans l'avionique, nottamment sur l'A380, sont faits avec SCADE. C'est une techno formelle et synchrone basée sur lustre ( http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lang-design(...) ). Ca n'entre pas dans les questions d'interruptions, de tâches, etc qui sont gérées par un éventuel OS (certifié ou non, type greenhills http://www.ghs.com/(...) , lynuxworks http://www.lynuxworks.com/,(...) windriver VxWorks et j'en passe). Ca permet de faire des lois de commandes et des algos sûrs, sur lesquels ont peut faire assez "facilement" de la preuve formelle, de la couverture de modèle, etc. On est un niveau d'abstraction au dessus du C. Derrière on peut générer du C ou de l'ADA, tout en concervant une excellente tracabilité (absolument nécessaire pour la certification DO-178B). J'arrête de m'étendre, pour plus d'infos aller voir là
Concernant TTech, c'est assez complémentaire avec SCADE, c'est un générateur de scheduling statique: on donne les temps d'execs maximums, les priorités et périodicités, et ça pond un code qui appelle les différentes taches dans le on ordre.
Note: je suis le webmaster du site en question, je le passe doucement aux standards, si vous avez des remarques, n'hésitez pas ( webmaster at esterel dash technologies dot com )
[^] # Re: Je ne veux pas être rabat-joie mais...
Posté par Obi MO (site web personnel) . En réponse au journal Vive GNU/linux & Airbus A380. Évalué à 2.
Effectivement, certaines morceaux du code emarqué critique dans l'avionique, nottamment sur l'A380, sont faits avec SCADE. C'est une techno formelle et synchrone basée sur lustre ( http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lang-design(...) ). Ca n'entre pas dans les questions d'interruptions, de tâches, etc qui sont gérées par un éventuel OS (certifié ou non, type greenhills http://www.ghs.com/(...) , lynuxworks http://www.lynuxworks.com/,(...) windriver VxWorks et j'en passe). Ca permet de faire des lois de commandes et des algos sûrs, sur lesquels ont peut faire assez "facilement" de la preuve formelle, de la couverture de modèle, etc. On est un niveau d'abstraction au dessus du C. Derrière on peut générer du C ou de l'ADA, tout en concervant une excellente tracabilité (absolument nécessaire pour la certification DO-178B). J'arrête de m'étendre, pour plus d'infos aller voir là
http://www.esterel-technologies.com/products/scade-suite/overview.h(...)
</publireportage>
Concernant TTech, c'est assez complémentaire avec SCADE, c'est un générateur de scheduling statique: on donne les temps d'execs maximums, les priorités et périodicités, et ça pond un code qui appelle les différentes taches dans le on ordre.
Note: je suis le webmaster du site en question, je le passe doucement aux standards, si vous avez des remarques, n'hésitez pas ( webmaster at esterel dash technologies dot com )