Cyrille Comar, Adacore : "Ada a une belle carte à jouer dans les systèmes critiques de demain"

Le langage Ada fait partie depuis de nombreuses années du paysage des langages de programmation, au même titre que le C/C++ ou Java, apparu plus récemment. Moins connu que ces derniers, il a cependant su se faire un nom dans le monde des applications critiques à haut niveau de fiabilité pour les domaines de la Défense et des transports (aéronautique, espace, ferroviaire). L’évolution Ada 2012 lui ouvre aujourd’hui de nouvelles perspectives et un bel avenir; notamment pour des applications critiques, où la notion de sécurité devient primordiale. Cyrille Comar, l'un des fondateurs de la société AdaCore, analyse cette tendance. ...

Ada 2012, la dernière version du langage Ada, a été officiellement avalisée par l’ISO en fin d’année dernière. Quelles sont les évolutions majeures d’Ada 2012, par rapport à Ada 2005, la dernière révision du langage ? CYRILLE COMAR L’évolution la plus importante est que désormais Ada intègre la notion de programmation par contrat, que l’on trouvait notamment dans le langage Eiffel. Il s’agit dans un programme d’insérer un code spécifique, sous forme d’assertions, qui indique ce que l’utilisateur doit attendre comme résultat de son code, confor- mément aux spécifications. En d’autres termes, il s’agit d’associer au sein du code, de manière standardisée, les spécifi- cations de bas niveau ou tout au moins une partie de celles-ci. Ainsi, dans Ada 2012, on trouve en termes de programmation les notions de “précondition”, de “post- condition”, d’“invariant” qui sont autant de moyens de définir les obligations et les attentes d’un sous-programme, d’un type ou d’une portion de code vis à-vis des spécifications. L’objectif étant de pouvoir vérifier et déboguer son programme avec un maximum d’efficacité. En effet, grâce à cette notion de programmation par contrat, on peut espérer prouver de 50 à 80% d’un code par analyse statique complètement automatique, en laissant le reste aux tests classiques en dynamique. Cette approche de mixage des techniques de vérification est d’ailleurs l'un des objectifs du projet de recherche Hi-Lite qui a été conduit au sein du pôle de compétitivité Systematic et qui s’achèvera au mois de mai de cette année. C’est une voie de développement très importante car, dans les systèmes critiques, les temps et les coûts de vérification d’un programme sont devenus très importants. En proposant, d’une part, de fiabiliser les tests en prouvant mathématiquement que le code est bon, et, d’autre part, de diminuer les temps de test, Ada devient un langage de choix pour toutes les applications à haut niveau de criticité, que l’on retrouve au-delà de l’avionique, dans les transports, l’automobile ou l’industrie, le nucléaire en particulier.   La notion de sécurité devient très importante dans les applications embarquées critiques de plus en plus connectées au monde extérieur. Ada est-il adapté pour répondre à cette nouvelle problématique ? CYRILLE COMAR Nous pensons très fortement qu’Ada peut jouer un rôle important vis-à-vis de la sécurité. Certes, la sécurité d’un système est une notion large qui engage bien au-delà du code embarqué. Néanmoins, avec Ada 2012, on est capable d’apporter la notion de preuve formelle, donc de garantie d’une absence de risque vis-à-vis d’une attaque extérieure. D’ailleurs, c’est avec ces notions de preuve formelle que certains systèmes d’exploitation temps réel ont été certifiés aux niveaux EAL6, EAL6+,¨voire EAL7.   Pensez vous qu’Ada 2012 est bien positionné vis-à-vis de la nouvelle norme de certification DO-178C pour l’avionique ? CYRILLE COMAR Les standards de certification portent essentiellement sur la manière de développer un système et sur les vérifications et garanties que l’on apporte sur le bon fonctionnement de ce système. Dans ce cadre, Ada 2012 est une aide dans la démarche. De plus, la DO-178C s’intéresse, à travers le supplément DO-332, à la programmation orienté objet, et Ada est l'un des rares langages orientés objet qui permettra de prouver par le biais des méthodes de preuves formelles que les contraintes de sureté imposées par la nouvelle norme sur les constructions objets sont bien respectées. D’ailleurs, à la suite de ces évolutions dynamiques d’Ada, que l’on peut suivre sur le site ADA2012.org, nous voyons actuellement un mouvement de retour vers ce langage, notamment de la part d’organisations qui étaient plutôt parties sur Java ces dernières années.

Propos recueillis par François Gauthier