
Conduite automatisée : certaines puces-systèmes Nvidia vont migrer vers le RISC-V et les langages Ada et Spark L’éditeur franco-américain d’outils de développement et de vérification pour les logiciels de systèmes critiques AdaCore a dévoilé qu’il collaborait avec Nvidia. Objectif de cette association : implémenter les langages de programmation Ada et Spark dans des logiciels spécifiques de bas niveau critiques ...en termes de sécurité, utilisés par des applications aux contraintes très strictes de sécurité et du sûreté de fonctionnement comme la conduite automatisée et autonome. La collaboration entre AdaCore et Nvidia entre dans un cadre plus large où la société américaine a pris la décision de faire migrer certaines de ses familles de puces-systèmes SoC vers une nouvelle architecture bâtie sur le jeu d’instructions open source RISC-V et de mettre à niveau certains firmwares critiques en les réécrivant non plus en langage C mais en langages Ada et Spark. (On signalera au passage qu’AdaCore a rejoint récemment la Fondation RISC-V, lire notre article ici.) Les initiatives stratégiques de Nvidia visent à accroître les capacités de vérification de ses solutions pour obtenir la conformité aux exigences de la norme de sûreté de fonctionnement pour l’automobile ISO 26262. On rappellera que les langages Ada et Spark sont conçus pour répondre aux exigences logicielles les plus strictes en matière de sécurité et de sûreté. Très utilisé dans les secteurs de la Défense et de l’avionique, Ada dispose de caractéristiques intrinsèques qui permettent de détecter des défauts dans le code au tout débit du cycle de développement. De son côté, le langage Spark s’appuie sur un jeu restreint des propriétés d’Ada en vue d’apporter une preuve mathématique formelle et la certitude de repérer les erreurs dans le logiciel qui n’auraient pas pu être détectées par d’autres moyens. Spark facilite l’analyse statique qui peut démontrer de manière formelle certaines propriétés du code, de l’exactitude des flots de données et l’absence d’erreurs à l’exécution jusqu’à des assertions plus avancées et le respect des exigences fonctionnelles. « Les voitures autonomes sont particulièrement complexes et exigent des logiciels sophistiqués répondant aux standards les plus rigoureux dans ce domaine, indique Daniel Rohrer, vice-président en charge de la sécurité logicielle chez Nvidia. En prenant des mesures comme l’intégration des langages Ada et Spark dans nos plates-formes automobiles, nous améliorons la robustesse et l’assurance qualité vis-à-vis de la sécurité et de la sûreté. »

Conduite automatisée : certaines puces-systèmes Nvidia vont migrer vers le RISC-V et les langages Ada et Spark

L’éditeur franco-américain d’outils de développement et de vérification pour les logiciels de systèmes critiques AdaCore a dévoilé qu’il collaborait avec Nvidia. Objectif de cette association : implémenter les langages de programmation Ada et Spark dans des logiciels spécifiques de bas niveau critiques ...en termes de sécurité, utilisés par des applications aux contraintes très strictes de sécurité et du sûreté de fonctionnement comme la conduite automatisée et autonome.

La collaboration entre AdaCore et Nvidia entre dans un cadre plus large où la société américaine a pris la décision de faire migrer certaines de ses familles de puces-systèmes SoC vers une nouvelle architecture bâtie sur le jeu d’instructions open source RISC-V et de mettre à niveau certains firmwares critiques en les réécrivant non plus en langage C mais en langages Ada et Spark. (On signalera au passage qu’AdaCore a rejoint récemment la Fondation RISC-V, lire notre article ici.) Les initiatives stratégiques de Nvidia visent à accroître les capacités de vérification de ses solutions pour obtenir la conformité aux exigences de la norme de sûreté de fonctionnement pour l’automobile ISO 26262.

On rappellera que les langages Ada et Spark sont conçus pour répondre aux exigences logicielles les plus strictes en matière de sécurité et de sûreté. Très utilisé dans les secteurs de la Défense et de l’avionique, Ada dispose de caractéristiques intrinsèques qui permettent de détecter des défauts dans le code au tout débit du cycle de développement. De son côté, le langage Spark s’appuie sur un jeu restreint des propriétés d’Ada en vue d’apporter une preuve mathématique formelle et la certitude de repérer les erreurs dans le logiciel qui n’auraient pas pu être détectées par d’autres moyens. Spark facilite l’analyse statique qui peut démontrer de manière formelle certaines propriétés du code, de l’exactitude des flots de données et l’absence d’erreurs à l’exécution jusqu’à des assertions plus avancées et le respect des exigences fonctionnelles.

« Les voitures autonomes sont particulièrement complexes et exigent des logiciels sophistiqués répondant aux standards les plus rigoureux dans ce domaine, indique Daniel Rohrer, vice-président en charge de la sécurité logicielle chez Nvidia. En prenant des mesures comme l’intégration des langages Ada et Spark dans nos plates-formes automobiles, nous améliorons la robustesse et l’assurance qualité vis-à-vis de la sécurité et de la sûreté. »