S'inscrire aux newsletters

Article précédent

Sécurité des systèmes embarqués

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

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

Auteur(s) : Emmanuelle ENCRENAZ-TIPHENE

Date de publication : 10 févr. 2013

Article suivant

Modélisation et analyse de systèmes embarqués ou temps-réel avec le profil UML MARTE

Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes (215 articles en ce moment)

Cette offre vous donne accès à :

Une base complète et actualisée d'articles validés par des comités scientifiques

Un service Questions aux experts et des outils pratiques

ABONNEZ-VOUS

Quitter la lecture facile

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

Lire l’article

MOTS-CLÉS

Panorama | Systèmes embarqués | Informatique | électronique | Automatique

KEYWORDS

review | Embedded systems | computer science | electronics | engineerings

PERMALIEN

https://www.techniques-ingenieur.fr/base-documentaire/technologies-de-l-information-th9/systemes-embarques-42588210/methodes-formelles-pour-la-verification-des-systemes-embarques-h8250/

RÉFÉRENCE BIBLIOGRAPHIQUE

Exportez la référence bibliographique

Lire l’article

Lire l'article

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

Introduction aux systèmes embarqués.
OS embarqués.
Méthode B pour la spécification et la réalisation de logiciels et de systèmes critiques prouvés.

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

Lire l’article

DÉTAIL DE L'ABONNEMENT :

TOUS LES ARTICLES DE VOTRE RESSOURCE DOCUMENTAIRE

Accès aux :

Articles et leurs mises à jour

Nouveautés

Archives

Formats :

HTML illimité

Versions PDF

Site responsive (mobile)

Info parution :

Toutes les nouveautés de vos ressources documentaires par email

DES SERVICES ET OUTILS PRATIQUES

Questions aux experts

Les meilleurs experts techniques
et scientifiques vous répondent

Articles Découverte

La possibilité de consulter des
articles en dehors de votre offre

Dictionnaire technique multilingue

45 000 termes en français, anglais,
espagnol et allemand

Votre site est 100% responsive,
compatible PC, mobiles et tablettes.

FORMULES

	Formule monoposte	Autres formules
Ressources documentaires
Consultation HTML des articles	Illimitée	Illimitée
Téléchargement des versions PDF	5 / jour	Selon devis
Accès aux archives	Oui	Oui
Info parution	Oui	Oui

Services inclus
Questions aux experts (1)	4 / an	Jusqu'à 12 par an
Articles Découverte	5 / an	Jusqu'à 7 par an
Dictionnaire technique multilingue	Oui	Oui
(1) Non disponible pour les lycées, les établissements d’enseignement supérieur et autres organismes de formation.
	Formule 12 mois monoposte 1 905 € HT AJOUTER AU PANIER	Autres formules (Multiposte, pluriannuelle) DEMANDER UN DEVIS

AJOUTER AU PANIER

DEMANDER UN DEVIS

Sommaire
Sommaire détaillé

INTRODUCTION

1 - CONCEPTION DES SYSTÈMES EMBARQUÉS

2 - BESOINS DE GARANTIES

2.1 - Motivations
2.2 - Intégration de la vérification dans le flot de conception
2.3 - Différents types de vérification

3 - MÉTHODES FORMELLES POUR LA VÉRIFICATION FONCTIONNELLE

3.1 - Preuve assistée
3.2 - Model-Checking
3.3 - Analyse statique

4 - AIDE À LA VALIDATION (PAR SIMULATION)

4.1 - Différents types de tests
4.2 - Génération de séquences de test
4.3 - Moniteurs pour vérification dynamique

5 - CONCEPTION SÛRE GARANTIE PAR CONSTRUCTION

5.1 - Principe de la méthode B
5.2 - Réalisations concrètes

6 - CONCLUSION

Publicité Devenez annonceur

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

RÉSUMÉ

ABSTRACT

Auteur(s)

INTRODUCTION

MOTS-CLÉS

KEYWORDS

PERMALIEN

RÉFÉRENCE BIBLIOGRAPHIQUE

BIBLIOGRAPHIE

DANS NOS BASES DOCUMENTAIRES

ANNEXES

SUR LE MÊME SUJET

DANS LES RESSOURCES DOCUMENTAIRES

DANS L'ACTUALITÉ

DANS LES LIVRES BLANCS

DANS LES CONFÉRENCES EN LIGNE

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

RÉSUMÉ

ABSTRACT

Auteur(s)

INTRODUCTION

MOTS-CLÉS

KEYWORDS

PERMALIEN

RÉFÉRENCE BIBLIOGRAPHIQUE

La lecture complète de cet article et le téléchargement du PDF sont réservés aux abonnés

BIBLIOGRAPHIE

DANS NOS BASES DOCUMENTAIRES

ANNEXES

La lecture complète de cet article et le téléchargement du PDF sont réservés aux abonnés

SUR LE MÊME SUJET

DANS LES RESSOURCES DOCUMENTAIRES

DANS L'ACTUALITÉ

DANS LES LIVRES BLANCS

DANS LES CONFÉRENCES EN LIGNE