Prêtable
| Titre : | Systèmes temps réel 1 : Techniques de description et de vérification |
| Auteurs : | Nicolas Navet |
| Type de document : | texte imprimé |
| Editeur : | Paris [France] : Lavoisier, 2006 |
| Collection : | Traité IC2 (Série : informatique et systèmes d'information), Dirigée par : Jean-Charles, Pomerol |
| ISBN/ISSN/EAN : | 978-2-7462-1303-6 |
| Format : | 370-VII p. / couv. en coul. / 24 cm. |
| Langues: | Français |
| Langues originales: | Français |
| Index. décimale : | 004.33 (Traitement en temps réel) |
| Catégories : | |
| Mots-clés: | Temps réel ; Méthodes formelles |
| Résumé : |
Aujourd'hui, les systèmes informatiques temps réel sont présents dans de multiples secteurs d'activités : contrôle des systèmes automatisés de production, aide à la conduite des véhicules ou gestion des flux d'information sur des réseaux locaux et sur l'Internet. Au cours des 30 dernières années, le temps réel s'est progressivement établi comme une discipline à part entière qui rassemble une forte communauté issue à la fois du monde académique et de l'industrie. Ce traité en deux volumes a pour objectif de mieux faire connaître cette discipline : ses enjeux, les méthodes et formalismes qui lui sont spécifiques, les outils existants, les résultats connus et, naturellement, les recherches encore à mener. Ce premier volume est consacré aux techniques de description et de vérification formelle, comme le model-checking, qui permettent de s'assurer, avant déploiement du système, du respect des propriétés de bon fonctionnement. Ce volume est délibérément orienté outils de façon à proposer des solutions concrètes à l'utilisateur potentiel de méthodes formelles.
|
| Note de contenu : |
Sommaire :
Chapitre 1: Réseaux de petri temporels : méthodes d'analyse et vérifications Chapitre 2: Combinaison entre vérification et test pour la validation de systèmes réactifs Chapitre 3: Model checking : éléments de base Chapitre 4: Vérification par automates temporisés Chapitre 5: Modélisation et analyse de systèmes asynchrones avec CADP Chapitre 6: Vérification de programmes synchrones avec Lustre/Lesar Chapitre 7: Lucid Synchrone, un langage de programmation des systèmes réactifs Chapitre 8: Vérification de systèmes probabilisés : méthodes et outils Chapitre 9: La boîte à outils IF pour la modélisation et la vérification de systèmes temps réels Chapitre 10: Description d'architectures pour le temps réel : l'approche AADL |
Exemplaires (2)
| Cote | Support | Localisation | Section | Disponibilité |
|---|---|---|---|---|
| F8/3612 | Livre | Bibliothèque de la Faculté de Technologie | Salle des livres | Disponible |
| F8/3613 | Livre | Bibliothèque de la Faculté de Technologie | Salle des livres | Disponible |
