AdaCore muscle ses outils de développement et de vérification pour la programmation à base de modèles

La société franco-américaine AdaCore, éditeur d’outils de développement et de vérification pour des logiciels à fortes contraintes de sûreté de fonctionnement, vient de faire évoluer son récent outil QGen, introduit ...sur le marché en 2015 et 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 (un sous-ensemble du langage Ada analysable via des méthodes formelles), 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.

Dans la version 2.1, QGen apporte une optimisation du code pour les blocs “switch”, la possibilité d’ajouter un code externe pour les tables de correspondance et les blocs dits “Prelookup”, la prise en charge des blocs commentés, ainsi que la  factorisation du code pour les modèles de référence et les bibliothèques de modèles. En outre, le support pour le débogage directement au niveau du modèle est disponible à l’état de prototype. Il s’agit ici, à l’aide de l’environnement de développement intégré GPS (GNAT Programming Studio) d’AdaCore, de déboguer les modèles écrits avec les outils Simulink ou Stateflow de MathWorks, ainsi que les applications utilisant à la fois du code préparé manuellement et du code généré automatiquement.

Parallèlement, la société met à disposition des utilisateurs la version 7.4 de son environnement de maintenance de code GNAT Pro qui inclut désormais un compilateur Ada complet et un débogueur visuel. Côté compilation, l’outil s’appuie sur les bases du compilateur en open source gcc 4.9 et, côté débogage, sur la technologie gdb 7.10. Il prend en charge Windows 10 ainsi que plusieurs nouvelles plates-formes cibles, notamment VxWorks 7 (ARM, e500v2, PPC, x86_64), VxWorks 653 3.0 et PikeOS (PowerPC). Au-delà, l’utilitaire au sein de GNAT Pro GNATtest génère désormais automatiquement des infrastructures de test unitaire prêtes à l’emploi, et la fonctionnalité de développement distribuée GPRbuild peut désormais s’appuyer sur des batteries de serveurs et/ou des processeurs multicœurs.