Avec Qgen, AdaCore facilite la génération de code certifiable pour les modèles écrits en Simulink

AdaCore Qgen

Le franco-américain AdaCore a profité du salon Embedded World qui se tient cette semaine à Nuremberg pour annoncer la sortie de l'outil Qgen 1.0 qui est à la fois un générateur de code qualifiable et un vérificateur de modèles ...écrits au sein des environnements Simulink et Stateflow de MathWorks. Cet outil original est capable de générer soit du code Ada conforme aux spécifications Spark, soit du code Ansi C respectant les règles Misra C, avec dans les deux cas la volonté d'obtenir du code lisible et traçable. Une approche qui vise les applications critiques temps réel à haut niveau de sûreté de fonctionnement qui doivent la plupart du temps respecter des normes de certification et qui sont développées avec une méthodologie basée modèles. Avec en arrière-plan la volonté de diminuer fortement les coûts de certification pour cette catégorie de développeurs.

Pour ce faire, Qgen fonctionne sur un sous-ensemble de Simulink, à savoir sur une centaine de blocs de fonction (et quelques opérations arithmétiques de Matlab) soigneusement choisis par AdaCore selon trois critères. Ces blocs génèrent en effet du code exécutable stable et prévisible, ne nécessitent pas de support spécifique au niveau de leur runtime et enfin sont adaptés aux contraintes des opérations de certification. Le code généré par Qgen à partir d'un programme écrit avec ces blocs s'avère ainsi, selon AdaCore, aisément certifiable vis-à-vis des spécifications DO-178 (avionique), EN 50128 (ferroviaire) et ISO 26262 (automobile). Au-delà, la société compte obtenir avant la fin 2015 une qualification complète de son outil vis-à- vis de la norme DO-178C jusqu'au niveau 5 (TQL5, l'équivalent de la notion d'outil de développement dans la DO-178B).

Au niveau fonctionnel, Qgen est aussi capable de vérifier les modèles écrits en Simulink grâce à des technologies d'analyse statique de code propres à AdaCore (écran ci-contre). Objectif  : détecter au sein des modèles les problèmes d'erreurs de runtime comme les divisions par zéro ou le dépassement d'entier (integer overflow), mettre en évidence des erreurs logiques comme du code mort (dead execution paths) et enfin vérifier les propriétés fonctionnelles des blocs d'assertion de Simulink, spécifiquement dédiés à la vérification formelle d'un modèle. Pour ceux qui le souhaitent, Qgen peut aussi être intégré avec les outils GNATemulator et GNATcoverage d'AdaCore afin de réaliser des tests du type PIL (Processor-in-the-Loop) et une couverture structurelle du code sans avoir à l'instrumenter. Une des caractéristiques de l'outil est qu'il est configurable, grâce à la représentation intermédiaire qu'il génère, visible par les développeurs. Enfin, signalons que le support des modèles développés avec l'outil Stateflow de MathWorks, environnement de modélisation et de simulation à partir de l'écriture de machines d'état, est prévu pur la fin du second trimestre 2015.

« Qgen  procure deux types d'opportunités à notre société, déclare Cyrille Comar, président d'AdaCore. D'abord les utilisateurs de nos technologies peuvent désormais bénéficier de la génération de code certifiable à partir de modèles Simulink/Stateflow sans avoir à modifier leurs investissements, et ensuite, cet outil nous rapproche d'une base d'utilisateurs importante qui travaillen dans des domaines où la sécurité du code est critique et qui ne connaît pas forcément notre expertise en code à très haut niveau de sûreté focntionnelle. »