MtoM Mag - Le journal de l'MtoM.
- accueil .
- newsletter .
Flux RSS . - soumissions .
- publicité .
- contacts
Flux RSS .
L’impact de la complexité sur la fiabilité des logiciels critiques : La taille et la complexité des logiciels dans les systèmes critiques augmentent à un rythme étonnant. Avions, automobiles, appareils médicaux, applications d’infrastructure, des systèmes qui étaient autrefois uniquement matériels dépendent aujourd’hui de logiciels pour une grande partie de leurs fonctionnalités. Dans ces cas, la vérification du bon fonctionnement des logiciels est un enjeu majeur.
Les défauts non découverts dans les logiciels de systèmes critiques peuvent entraîner une défaillance catastrophique, des pertes de vies humaines, de graves dommages liés à une vulnérabilité au hacking.
Le niveau d’exigence est très élevé : la probabilité maximale requise de défaillance des éléments les plus critiques de ces systèmes peut être de l’ordre de 10-7 à moins de 10-9 défaillances par heure.
Les méthodes de test conventionnelles sont insuffisantes car elles ne peuvent établir que la présence de défauts, et non leur absence. Pour démontrer une probabilité d’erreur de <10-9 les essais requis devraient durer des centaines d’années voire des centaines de milliers ou des millions d’années selon les hypothèses. Les tests traditionnels ne peuvent pas garantir le niveau de fiabilité requis par les systèmes critiques car il y a tout simplement trop de combinaisons à couvrir
Les méthodes formelles sont nécessaires pour vérifier les logiciels critiques Aujourd’hui, de grandes organisations trouvent le moyen de remédier à ce problème en utilisant les méthodes formelles. Longtemps considérées comme peu pratiques ou trop chères pour les logiciels commerciaux, les méthodes formelles ont atteint leur maturité grâce aux progrès de la puissance de calcul et de nouveaux outils qui automatisent et simplifient leur application. Contrairement aux tests, qui échantillonnent le comportement des logiciels afin de révéler les défauts, les méthodes formelles analysent le comportement du logiciel et établissent la présence ou l’absence de défauts. Les développeurs peuvent ainsi identifier des conditions spécifiques qui doivent ou ne doivent pas se produire et utiliser des méthodes formelles pour prouver que ces conditions se produisent toujours ou jamais.
Toute organisation qui développe des logiciels critiques pour répondre aux normes de fiabilité les plus élevées c’est-à-dire des logiciels dont la défaillance est inacceptable tirera profit de l’utilisation de méthodes formelles de vérification.
De nombreuses applications sont concernées, parmi lesquelles les modules critiques pour la sécurité dans les domaines de l’avionique, des dispositifs médicaux, pour le contrôle des véhicules automobiles, le contrôle et la surveillance de centrales d’énergie nucléaire, les applications d’infrastructures critiques comme la distribution d’énergie et la commutation des télécommunications, les applications de données sécurisées ainsi que les composants informatiques critiques comme les noyaux de systèmes d’exploitation.
Différentes solutions de méthodes formelles existent. Pour faire son choix, AdaCore recommande de prendre en compte les éléments suivants :
La bonne balance entre l’expressivité et l’automatisation. L’expressivité fait référence à la facilité avec laquelle les développeurs peuvent décrire la fonctionnalité souhaitée dans un langage formel donné. L’automatisation fait référence à la facilité avec laquelle les outils de méthodes formelles peuvent effectuer une analyse sans l’aide d’un humain. En général, une plus grande expressivité se traduit par une automatisation moindre.
La solidité, c’est-à-dire la précision et la fiabilité des résultats d’analyse. Si une méthodologie ou un outil prétend vérifier une propriété donnée d’un programme (par exemple, qu’un index dans un tableau se trouve dans les limites du tableau), il doit alors détecter toute violation de cette propriété. C’est une caractéristique essentielle des méthodes formelles.
Les possibilités d’intégration. Les méthodes formelles offrent généralement des bibliothèques de tâches de programmation courantes beaucoup plus petites que celles des langages de programmation traditionnels. Les développeurs devront donc être capables d’intégrer la partie du logiciel écrite dans le langage formel avec la partie du logiciel qui dépend des bibliothèques existantes
L’adoption d’une procédure incrémentale. Les méthodes formelles peuvent être déployées progressivement dans le cadre d’efforts de développement de logiciels existants.
La qualité de l’outillage et du support aux développeurs. De nombreuses méthodes formelles ne sont pas développées ou supportées de manière professionnelle, ce qui peut remettre en question leur adoption pour le développement de logiciels industriels.
La qualité de la communauté d’utilisateurs actifs. C’est un point important pour les méthodes formelles, autant qu’il peut l’être pour les langages de programmations classique.
