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.
« 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é. »
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. CCGpermet 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. »
A propos d’ISO 26262 et ASIL D
La norme ISO 26262 est une norme de sûreté fonctionnelle pour les systèmes automobiles et un dérivé de la norme générique CEI 61508 pour les systèmes électriques / électroniques / électroniques programmables ("E/E/EP"). Elle définit les phases du cycle de vie de la sûreté automobile et leurs activités associées et utilise une approche fondée sur le risque pour déterminer les niveaux d'intégrité de la sûreté automobile (ASIL) et les exigences correspondantes. Une analyse des fonctions du système se concentre sur les dangers potentiels en cas de défaillance et sur les conséquences pour la vie et les biens. L'ASIL calculé va de A (le moins critique) à D (le plus critique) et prend en compte la probabilité estimée que la défaillance soit exposée, la possibilité pour le conducteur d’atténuer le danger en réponse et la gravité de l'occurrence du danger. ASIL D représente le potentiel probable de blessure grave, voire mortelle, en cas de dysfonctionnement. Elle exige donc d’assurer au plus haut niveau que les objectifs de sûreté sont suffisants et ont été atteints.
A propos de JTEKT
JTEKT Corporation a été créée en 2006 par la fusion de Koyo Seiko, Ltd, un fabricant de roulements de classe mondiale, et de Toyoda Machine Works, Ltd, un fabricant de machines-outils excellant dans les technologies de pointe.
Combinant les technologies les plus avancées et la passion de la fabrication des deux sociétés, JTEKT est aujourd'hui un fournisseur de systèmes de confiance de composants automobiles, de roulements et de machines-outils, fournissant aux clients des produits et des technologies de classe mondiale qui se traduisent par des contributions continues à la société.