AdaCore, éditeur franco-américain d’outils de développement et de vérification logiciels pour applications critiques, anonce la disponibilité opérationnelle des langages de programmation formelle Ada et Spark (*) sur le marché automobile, et ce en collaboration avec Nvidia.

Les deux sociétés s'apprêtent ainsi à publier gratuitement leur solution à destination des développeurs qui souhaitent suivre leur approche, sous forme de documents en open source, évolutifs et prêts à l’emploi.

Selon AdaCore, alors que la valeur ajoutée de l'industrie automobile se déplace de plus en plus des fonctionnalités mécaniques vers les fonctionnalités logicielles, atteindre un niveau de sécurité logiciel optimal devient l'un des défis majeurs du développement automobile moderne. Dans ce contexte, Nvidia a développé Drive OS, un système d'exploitation avec sa pile logicielle associée, spécifiquement conçu pour le développement et le déploiement d'applications installées sur le circuit Drive AGX de la société, destiné au domaine de la conception de véhicules autonomes.

Cet ensemble intègre notamment des composants logiciels conformes aux plus hauts niveaux d'intégrité de la norme automobile ISO-26262.

C'est dans ce cadre que Nvidia a sélectionné les langages Ada et Spark pour développer certains des composants les plus critiques de cette pile logicielle. Ce qui a nécessité, précise la socété, la mise en place d'un processus de développement exploitant les méthodes formelles et autres caractéristiques de sécurité spécifiques aux langages Ada et Spark. L’objectif étant ici d’exploiter pleinement leurs capacités.

Le processus de référence ISO-26262 d’AdaCore et de Nvidia est d’ores est déjà partiellement disponible sur la plate-forme GitHub et peut être utilisé ou personnalisé librement par toute personne souhaitant adopter ces langages.

(*) Le langage Spark s’appuie sur un jeu restreint des propriétés du langage Ada en vue d’apporter une preuve mathématique formelle et la certitude de repérer les erreurs dans un logiciel qui n’auraient pas pu être détectées par d’autres moyens.