Prêtable
| Titre : | Vérification et mise en oeuvre des réseaux de petri |
| Auteurs : | Michel Diaz |
| Type de document : | texte imprimé |
| Editeur : | Paris [France] : Lavoisier, 2003 |
| Collection : | Traité IC2 Information-commande-communication (Série : Systèmes automatisés), Dirigée par : Foulard, Claude |
| ISBN/ISSN/EAN : | 978-2-7462-0445-4 |
| Format : | 389 p. / ill.; couv. ill. en coul. / 24 cm. |
| Langues: | Français |
| Langues originales: | Français |
| Index. décimale : | 511.35 (Théorie de la récurrence) |
| Catégories : | |
| Mots-clés: | Réseaux petri ; Logique linéaire ; Automatique de programme |
| Résumé : |
Les réseaux de Petri portait sur la modélisation des systèmes dont les comportements dépendent de valeurs temporelles. Cette étude avait permis de définir les RdP Temporels ainsi qu'une nouvelle approche sémantique pour analyser les fonctionnements généraux et les RdP Stochastiques à partir desquels de nombreux travaux ont permis d'évaluer les performances et la fiabilité des systèmes. Le présent ouvrage insiste sur la vérification et la mise en oeuvre des modèles fondamentaux exposés dans l'ouvrage précédent.
Il se compose de trois parties. La première valide les propriétés spécifiques des systèmes conçus en se fondant sur la construction et l'analyse du graphe d'accessibilité, graphe représentant tous les comportements possibles. La seconde partie aborde la vérification explicite des comportement temporels c'est-à-dire les comportements liés aux valeurs explicites des variables temporelles entrant dans la définition des systèmes à temps contraints. La troisième partie présente de nombreuses études de cas dans des domaines ayant un intérêt essentiel. Des solutions pour les systèmes réels sont ainsi avancées : elles sont le résultat de modélisations et d'applications significatives dans des domaines d'application en fort développement : télécommunication, programmation, multimédia... |
| Note de contenu : |
Sommaire :
Partie 1: Vérification et maitrise de l'explosion combinatoire Chapitre 1: Vérification et maîtrise de l'explosion combinatoire Chapitre 2: Vérification de propriétés spécifiques Chapitre 3: Graphes de pas couvrants : une approche ordre partiel Chapitre 4: Dépliages pour la vérification de propriétés temporelles Chapitre 5: Symétries et logique temporelle Partie 2: Vérification et analyse temporelle. Chapitre 6: Les réseaux de Petri hiérarchisés à flux temporels Chapitre 7: Réseaux de Petri et logique linéaire Partie 3: Étude de cas. Chapitre 8: Modélisation et vérification de l'interopérabilité de services de télécommunication Chapitre 9: Application des réseaux de haut niveau à la vérification automatique de programmes ADA 95 concurrents Chapitre 10: Modélisation et implémentation d'architectures multimédias Chapitre 11: Évaluation des performance en productique Chapitre 12: Évaluation de performances de protocoles de communications |
Exemplaires (2)
| Cote | Support | Localisation | Section | Disponibilité |
|---|---|---|---|---|
| F8/2260 | Livre | Bibliothèque de la Faculté de Technologie | Salle des livres | Disponible |
| F8/2261 | Livre | Bibliothèque de la Faculté de Technologie | Salle des livres | Disponible |
