En poursuivant votre navigation sur ce site, vous acceptez l'utilisation de cookies pour vous proposer des contenus et services adaptés à vos centres d'intérêts. En savoir plus et gérer ces paramètres. OK X
 
 

 

 

Nouveaux produits

AdaCore : JTEKT choisit SPARK Pro pour ses logiciels automobiles critiques

Publication: Juin 2020

Partagez sur
 
Des méthodes formelles aident JTEKT à réduire les coûts de développement et de vérification des systèmes de conduite autonome sûrs...
 

AdaCore a annoncé aujourd’hui que JTEKT, une société internationale de fabrication de systèmes de direction assistée électrique pour l’automobile dont le siège se situe au Japon, a adopté la suite logicielle SPARK Pro et GNAT Pro Common Code Generator (CCG) d’AdaCore pour aider au développement de logiciels critiques de systèmes de direction assistée. Profitant du programme de mentorat d’AdaCore destiné à l’aider à se mettre rapidement à niveau avec la technologie SPARK, JTEKT a démontré de quelle façon exploiter le sous-ensemble de langage SPARK Ada et les méthodes formelles pour faciliter les tests unitaires et la vérification du code C du système afin de s’assurer qu’il est correct. L’utilisation de CCG, qui compile SPARK en code source C, a permis à JTEKT de tirer pleinement parti de SPARK pour prouver ses propriétés de sûreté critiques tout en utilisant son infrastructure C existante.

Le logiciel de commande de direction assistée d’un système de direction doit contrôler et fonctionner en toute sécurité avec d’autres systèmes de conduite autonomes, tels que l’assistance au maintien de la trajectoire. En raison du risque de blessure grave ou mortelle en cas de dysfonctionnement, ces systèmes sont classés au niveau d’intégrité de sûreté automobile (ASIL) D - la classification la plus stricte du danger initial (risque de blessure) définie dans la norme ISO 26262.

SPARK Pro est un ensemble d’outils basé sur le sous-ensemble SPARK formellement analysable du langage Ada, permettant aux développeurs de garantir les propriétés du code source avec une rigueur mathématique. Grâce à SPARK Pro, les développeurs peuvent prouver l’absence de certaines catégories de vulnérabilités (telles que le débordement de mémoire, la division par zéro et les références à des variables non initialisées) et également prouver des assertions fonctionnelles personnalisées. CCG permet aux projets de réaliser une compilation croisée des applications SPARK vers n’importe quelle cible matérielle fournissant un compilateur C, y compris les cibles qui ne sont pas fournies avec un support Ada standard. SPARK Pro et CCG sont tous deux qualifiés selon les normes de sûreté fonctionnelle ISO 26262 et IEC 61508.

« Nous étudions depuis quelques années des méthodes formelles pour répondre aux demandes actuelles de l’industrie automobile en matière de logiciels, à savoir une grande fiabilité avec une bonne justification de sûreté, et nous avons été ravis d’apprendre l’existence de SPARK », a déclaré Shinya Yoneki, Directeur du Développement de Systèmes Avancés chez JTEKT, au Japon. « Nous pensons que les outils d’AdaCore nous permettront de réaliser des économies sur les tests de logiciels critiques pour la sûreté et nous aideront à terme à produire en masse un code sûr et sécurisé. »

« L’utilisation de méthodes formelles pour garantir l’exactitude du code C généré par SPARK est à la pointe de la technologie en matière de sûreté automobile », a déclaré Juan Carlos Bernedo, Directeur des Ventes d’AdaCore au Japon. « SPARK est rapidement en train de devenir une solution rentable de choix pour les développeurs de logiciels qui doivent répondre aux normes d’assurance les plus élevées de l’industrie automobile, et l’expérience de JTEKT montre comment un fournisseur de logiciels centré sur C peut introduire et exploiter avec succès le langage et les outils SPARK. »

http://www.adacore.com/

Suivez Industrie Mag sur le Web

 

Newsletter

Inscrivez-vous a la newsletter d'Industrie Mag pour recevoir, régulièrement, des nouvelles du site par courrier électronique.

Email: