Bibliographie & annexes
Présentation
En anglais
RÉSUMÉ
Les systèmes embarqués sont soumis à de nombreuses contraintes et certains sont en interaction étroite avec des procédés dangereux ou interviennent dans des processus de décisions impactant des vies humaines. Pour augmenter le degré de confiance en ces systèmes, plusieurs méthodes formelles peuvent être mises en oeuvre : la démonstration assistée de preuve, l'examen automatisé des comportements du système ou le raffinement de spécification. Dans chaque cas, on présente le principe, les principaux outils académiques et certains outils industriels ainsi que les réalisations pratiques.
Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.
Lire l’articleABSTRACT
Embedded systems are subjected to a large number of constraints and certain are closely linked with hazardous processes or are involved in decision-making processes which impact human lives. In order to increase the degree of trust in these systems, several formal methods can be implemented: theorem proving, automated scrutiny of the system or specification refinement. In each case, the principle, major academic tools, certain industrial tool and practical achievements are presented.
Auteur(s)
-
Emmanuelle ENCRENAZ-TIPHENE : Ingénieur de l'École polytechnique féminine - Maître de conférences à l'Université Pierre et Marie Curie, Paris
INTRODUCTION
Les systèmes embarqués sont soumis à de nombreuses contraintes et certains sont en interaction étroite avec des procédés dangereux ou interviennent dans des processus de décisions impactant des vies humaines. Le développement de tels systèmes doit offrir des garanties de bon fonctionnement et de bon rétablissement en cas de défaillance d'une partie interne ou d'un environnement non prévu.
Des méthodes de vérifications formelles peuvent être mises en œuvre pour augmenter le degré de confiance des systèmes. Trois grandes classes se distinguent :
-
la preuve assistée (theorem-proving) ;
-
la vérification par modèle (model-checking) et ses nombreuses variantes et extensions ;
enfin le raffinement de spécification.
On présente le positionnement de ces approches dans le flot de conception des systèmes embarqués.
Pour chaque approche, on s'attache à présenter simplement le principe de base, le domaine applicatif principal, les outils disponibles ainsi que les réalisations académiques et industrielles. Cet article n'utilise pas de formalisme mathématique poussé pour être accessible au plus grand nombre. Les références bibliographiques permettent d'approfondir chaque approche tant sur les aspects formels que sur les outils disponibles ou (le cas échéant) leur utilisation dans un contexte industriel.
L'expertise technique et scientifique de référence
KEYWORDS
review | Embedded systems | computer science | electronics | engineerings
DOI (Digital Object Identifier)
Cet article fait partie de l’offre
Technologies logicielles Architectures des systèmes
(239 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Présentation
Conception sûre garantie par construction
En anglais
4. Aide à la validation (par simulation)
Si les méthodes formelles sont appliquées dans les processus requérant les plus hauts niveaux de garanties, elles ne peuvent pas toujours aboutir du fait de l'explosion combinatoire ou des surapproximations trop grossières à appliquer pour pouvoir conclure. Les méthodes de test (fonctionnel) restent très largement utilisées. Étant non exhaustives elles posent le problème de la sélection, parmi un ensemble infini de séquences de stimuli à appliquer, d'un sous-ensemble fini, extrêmement réduit, permettant de placer le système dans des configurations difficiles à atteindre et ayant été identifiées comme particulièrement sensibles. Les méthodes formelles peuvent intervenir pour aider au choix de ces séquences pertinentes et également pour construire des observateurs, analysant au fil de l'exécution des propriétés de la spécification du système.
4.1 Différents types de tests
On distingue différents types de test fonctionnel. Les tests de chaque composant (matériel ou logiciel) s'assurent de la conformité d'un élément vis-à-vis de sa spécification. Ces tests peuvent s'opérer aux interfaces des composants (sans présupposer de connaissance sur sa description interne (test en boîte noire), ou alors en disposant de la structure interne (test en boîte blanche). Les tests d'intégration s'assurent de la compatibilité des composants assemblés et de leur bonne coopération pour réaliser des fonctionnalités transverses. Ils peuvent également être en boîte noire ou boîte blanche (au niveau système). Les tests de non-régression s'assurent quant à eux qu'une modification (au niveau d'un composant ou d'une connexion entre composants) n'a pas dégradé le fonctionnement du système.
La qualité d'un test associe, à l'ensemble des séquences de stimuli injectés, une grandeur qualifiant sa pertinence. Lorsque l'on dispose d'une description algorithmique d'un composant, on peut chercher à construire des séquences de stimuli qui garantissent que toutes les instructions de l'algorithme sont exécutées (ce qui implique que tous les branchements sont pris au moins une fois et correspondent au niveau d'exigence DAL-D des critères communs). On peut aussi chercher à évaluer les conditions des alternatives pour toutes les configurations des variables qui composent leur expression (degré d'exigence DAL-A). Lorsque l'on s'intéresse à la vue externe d'un composant,...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Technologies logicielles Architectures des systèmes
(239 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Aide à la validation (par simulation)
BIBLIOGRAPHIE
-
(1) - ABRIAL (J.-R.) - The B-book : assigning programs to meanings. - Cambridge University Press New York, NY, USA © 1996 ISBN:0-521-49619-5 (1996).
-
(2) - BOUISSOU (O.) - Vérification partielle de programmes de contrôle-commande par interprétation abstraite. - Technique et Science informatiques, Lavoisier-Hermès, vol. 31, no 3, p. 337-374 (2012).
-
(3) - BRYANT (R.) - Graph-based algorithms for boolean function manipulation. - IEEE Trans. Computers, 35(8), p. 677-691 (1986).
-
(4) - CLARKE (E.) et al - Counter example-guided abstraction refinement. - CAV, p. 154-169 (2000).
-
(5) - CLARKE (E.) et al - Model checking and abstraction. - ACM-TOPLAS, vol. 16, no 5 (1994).
-
(6) - COOK (B.) et al - Terminator : beyond safety. - CAV 2006, p. 415-418...
DANS NOS BASES DOCUMENTAIRES
-
OS embarqués.
-
Méthode B pour la spécification et la réalisation de logiciels et de systèmes critiques prouvés.
Outil AbsInt analyse de programmes C par interprétation abstraite http://www.absint.com/profile.htm
Outil Astrée développé par le laboratoire LIENS pour l'analyse de programmes C et C++ par interprétation abstraite http://www.astree.ens.fr/
Projet BIP pour la connexion sûre de composants http://www-verimag.imag.fr/Rigorous-Design-of-Component-Based.html
Outil CADP développé par l'INRIA pour l'analyse par model-checking (de type équivalence d'automates) de systèmes asynchrones http://www.inrialpes.fr/vasy/cadp/
Chaînes de CAO de circuits Cadence® et Synopsis intégrant des outils de simulation et vérification fonctionnelle aux niveaux TLM, RTL http://www.cadence.com http://www.synopsys.com
Outil CVC4 SAT modulo Theory solver pour le bounded model-checking avec theories decidable http://www.cs.nyu.edu/acsys/cvc4/
Outil FoCS développé par le laboratoire de recherche de IBM-HAIFA pour la synthèse de moniteurs à partir de spécifications PSL http://www.research.ibm.com/haifa/projects/verification/focs/psl_vcs.html
Outil...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Technologies logicielles Architectures des systèmes
(239 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
