Article de référence | Réf : H8250 v1

Méthodes formelles pour la vérification fonctionnelle
Méthodes formelles pour la vérification des systèmes embarqués

Auteur(s) : Emmanuelle ENCRENAZ-TIPHENE

Date de publication : 10 févr. 2013

Pour explorer cet article
Télécharger l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !

Sommaire

Présentation

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’article

ABSTRACT

Formal methods for the verification of embedded systems

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.

Cet article est réservé aux abonnés.
Il vous reste 95% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

KEYWORDS

review   |   Embedded systems   |   computer science   |   electronics   |   engineerings

DOI (Digital Object Identifier)

https://doi.org/10.51257/a-v1-h8250


Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes

(233 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

ABONNEZ-VOUS

3. Méthodes formelles pour la vérification fonctionnelle

La vérification formelle des propriétés fonctionnelles d'un système consiste, à partir d'un modèle formel décrivant les comportements du système et d'un modèle de la spécification définissant des gabarits de comportements attendus, à déterminer, par un raisonnement mathématique (éventuellement automatisé dans un algorithme lorsque cela est possible) si les comportements du modèle du système sont conformes aux gabarits définis par la spécification.

Les différentes approches de vérification fonctionnelles varient en fonction :

  • de la nature du modèle à analyser ;

  • de la nature des propriétés à vérifier.

  • Nature du modèle à analyser. Le modèle peut être fini (par exemple, un protocole de cohérence de caches étudié pour un modèle à 5 caches) ou paramétré (le même protocole étudié pour un nombre n de caches, n étant un paramètre). Dans le premier cas l'ensemble des états accessibles du modèle est fini et on peut construire un algorithme qui les énumère. On se heurte à des problèmes d'explosion combinatoire de la taille de cet espace d'états. Dans le second cas, l'ensemble des états accessibles n'est pas borné et on ne peut pas définir un algorithme général qui parcourt automatiquement tous les états du système et permette de décider de la conformité des séquences du système par rapport à la spécification. On peut travailler sur des abstractions finies conservatives du modèle initial et retrouver des procédures de décision (donc automatisables) ou alors utiliser des méthodes de preuves manipulant les paramètres et requérant l'intervention de l'utilisateur pour guider la preuve lorsqu'il n'y a pas d'algorithme permettant de décider.

  • Nature des propriétés à vérifier. On distingue deux grandes classes de propriétés :

    – les propriétés de sûreté qui indiquent qu'un mauvais fonctionnement n'arrivera jamais ;

    Exemples

    « La variable x ne peut jamais dépasser la valeur 10 ».

    « Deux processus concurrents voulant accéder à une ressource critique ne pourront jamais y accéder simultanément ».

    « Le...

Cet article est réservé aux abonnés.
Il vous reste 92% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes

(233 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

ABONNEZ-VOUS

Lecture en cours
Méthodes formelles pour la vérification fonctionnelle
Sommaire
Sommaire

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

1 Outils logiciels

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...

Cet article est réservé aux abonnés.
Il vous reste 92% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes

(233 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

ABONNEZ-VOUS