Nvidia fait entrer Ada et SPARK dans les voitures autonomes
AdaCore et Nvidia ont développé un flux de référence open source pour les langages de programmation Ada et SPARK dans les logiciels automobiles critiques pour la sécurité, en particulier pour les voitures sans conducteur.
Ce flux permet d’accélérer le développement de logiciels ISO26262 sur le système d’exploitation DriveOS de Nvidia. Nvidia a développé DriveOS avec 7 millions de lignes de code en utilisant SPARK parallèlement au flux de certification pour les applications sur son matériel basé sur DRIVE AGX.
La puce AGX-Orin, basée sur l’architecture GPU Ampere et les cœurs ARM Cortex A78AE, est utilisée par des constructeurs automobiles tels que Volvo, Mercedes-Benz, Jaguar Landrover, GM, Zeekr et Geely et maintenant Toyota, le plus grand constructeur automobile du monde.
La puce AGX-Thor, basée sur l’architecture Blackwell avec des cœurs NeoverseV3AE, devrait être échantillonnée dans le courant de l’année pour la conduite autonome. Elle est utilisée par le fabricant chinois de véhicules électriques BYD, le fabricant de navettes autonomes WeRide, Volvo, le fabricant de camions Aurora, Continental et Li Auto.
DriveOS a été certifié ASIL-D par TUD SUD en janvier sur la puce Orin, avec un cadre de sécurité IA appelé Halos.
« Le temps des véhicules autonomes est arrivé et nous travaillerons avec l’IA dans la fabrication, les entreprises et la façon dont elles simulent et conçoivent les voitures et dans la voiture », a déclaré Jensen Huang, PDG de Nvidia. « Nous travaillons sur les voitures autonomes depuis plus d’une décennie ».
Le flux de référence constitue une avancée majeure et comprend des composants logiciels conformes aux niveaux d’intégrité les plus élevés de la norme de certification automobile ISO-26262. L’utilisation de SPARK a nécessité la mise en place d’un processus de développement qui tire parti des méthodes formelles et d’autres caractéristiques de sécurité du langage formel Ada et de son sous-ensemble SPARK.
AdaCore et Nvidia ont décidé de publier le processus de référence sous la forme d’un document ouvert et évolutif, permettant à l’industrie dans son ensemble d’adopter Ada et SPARK.
« Cela marque un tournant important pour les développeurs qui travaillent sur les véhicules définis par logiciel », explique à eeNews Europe Quentin Ochem, Chief Product and Revenue Officer chez AdaCore…
« Ce qui est unique ici, c’est l’approche de Nvidia. En adoptant Ada et SPARK et en publiant ouvertement sa documentation de qualification ISO 26262, Nvidia redéfinit la manière dont ces responsabilités sont assumées. Plutôt que d’imposer aux développeurs des activités de conformité abstraites et cloisonnées, Nvidia rapproche ces préoccupations de l’artefact principal du développeur : le code lui-même. Cette démarche s’inscrit dans une tendance croissante à intégrer la vérification, la traçabilité et les exigences directement dans le flux de développement, faisant de l’exactitude une propriété de la base de code, et non pas un processus distinct.
« Traditionnellement, les développeurs ont dû porter plusieurs chapeaux – au-delà de l’écriture du code, ils se retrouvent souvent à assumer les responsabilités d’ingénieurs d’assurance qualité, d’ingénieurs de vérification et même d’ingénieurs en charge des exigences », a-t-il ajouté.
« Les domaines critiques pour la sécurité comme l’automobile, régis par des normes telles que la norme ISO 26262, exigent une traçabilité rigoureuse, des preuves d’exactitude et une assurance formelle – des responsabilités qui vont bien au-delà de l’ingénierie logicielle conventionnelle ».
Il souligne également la décision de Nvidia d’ouvrir les artefacts de certification à la source, ce qui constitue une avancée majeure.
« Il est également rare de voir un grand fournisseur de technologie ouvrir à ce point son processus interne de certification de la sécurité. Le fait que la documentation ISO 26262 de Nvidia soit utilisable en l’état est un élément important : elle constitue un point de départ concret et pratique pour les autres équipes de développement de logiciels automobiles. Elle abaisse la barrière à l’entrée pour les développeurs et les entreprises qui souhaitent créer des logiciels automobiles sûrs et certifiés, sans avoir à réinventer la roue.
Le processus de référence ISO-26262 est disponible sur nvidia.github.io/spark-process/ et peut être utilisé ou personnalisé librement par toute personne intéressée par l’adoption de ces langages.
Processus ISO26262
Ce document définit un processus basé sur SPARK et conforme à la norme ISO-26262 pour le développement d’un sous-ensemble d’unités logicielles critiques pour la sécurité des véhicules jusqu’à l’ASIL D et à des ASIL inférieurs.
Le processus s’applique exclusivement aux unités logicielles développées entièrement dans le langage de programmation Ada, mais il est orienté vers les unités logicielles dont une partie ou la totalité du code Ada est conforme au sous-ensemble SPARK. Si certains éléments de ce processus, tels que les paramètres d’avertissement requis pour le compilateur Ada, peuvent s’appliquer au développement de logiciels Ada critiques pour la sécurité en général, une unité logicielle combinant Ada et d’autres langages (tels que C, C++ ou le langage d’assemblage) ne peut pas être développée à l’aide de ce processus.
Ce processus couvre les exigences et les objectifs de la norme ISO 26262 relatifs aux sous-ensembles de langage, à la conception des unités logicielles, à la mise en œuvre des unités logicielles et à la vérification des unités logicielles. En outre, le processus couvre les exigences et les objectifs de la norme ISO 26262 relatifs aux exigences de sécurité lorsqu’elles sont exprimées dans des spécifications d’interface logicielle.
Ce processus prend en charge la vérification formelle et la vérification non formelle côte à côte. Une unité logicielle unique développée selon ce processus peut faire l’objet d’une vérification formelle dans son intégralité, d’une vérification non formelle dans son intégralité, ou d’une vérification formelle partielle et d’une vérification non formelle partielle.
« En bref, cette initiative contribue à démystifier la certification de sécurité pour les développeurs et ouvre la voie à des architectures de véhicules définies par logiciel plus robustes et plus efficaces », a déclaré Ochem.
L’adoption d’un nouveau langage de programmation implique le déploiement d’un nouvel environnement, la formation des équipes à un nouveau formalisme, l’adaptation des modèles de programmation et bien d’autres choses encore. Cependant, du point de vue des processus, les langages de programmation sont largement interchangeables, mais Ada et SPARK, c’est une autre histoire.
L’envisager comme un changement de langage est une possibilité, et cela apporterait certainement de la valeur à un processus de développement traditionnel. Cependant, on passerait ainsi à côté de l’opportunité clé apportée par la technologie, à savoir la capacité de transformer le processus de développement en un processus axé sur la vérification, permettant de démontrer les propriétés du logiciel d’une manière beaucoup plus rigoureuse et rentable qu’avec les méthodes traditionnelles.
La sémantique Ada est conçue pour minimiser le risque de vulnérabilité et maximiser les informations sémantiques définies directement dans le code source. SPARK utilise ces attributs pour éviter les vulnérabilités courantes et permet de définir des propriétés supplémentaires à vérifier formellement à la place des tests dynamiques.
Dans SPARK, il est possible de garantir des propriétés de base telles que l’initialisation des variables, l’absence de débordement de mémoire tampon, l’étendue des données, ou plus généralement ce qui finirait autrement par être du code défensif. Mais il fournit également des moyens de définir des exigences plus avancées qui peuvent être exprimées sous la forme d’assertions booléennes, et par rapport auxquelles il est possible de démontrer formellement qu’une implémentation est correcte sans qu’il soit nécessaire d’exécuter des tests.
Développer du code en tenant compte de la vérification formelle a un impact à différents niveaux du processus de développement. La mise en place d’un moyen de développer des logiciels de cette manière peut être un long chemin itératif, avec le risque de passer à côté de certains aspects clés de la technologie.
Le flux de référence vise à permettre aux nouveaux adoptants de sauter cette étape et de commencer par un processus déjà établi qui a été examiné par les autorités et expérimenté par l’industrie. Il n’est pas destiné à être utilisé tel quel, mais à servir de point de départ à un processus personnalisé adapté à la situation spécifique de chaque organisation.
Cependant, Nvidia souligne que le flux ne couvre pas la spécification de la conception architecturale du logiciel, la manière de porter une unité logicielle C/C++ existante vers ce processus basé sur SPARK ou l’analyse de la concurrence ou de la sécurité du logiciel.
www.adacore.com ; nvidia.github.io/spark-process/
Si vous avez apprécié cet article, vous aimerez les suivants : ne les manquez pas en vous abonnant à :
