Titre :	Model checking
Type de document :	texte imprimé
Auteurs :	E. M. Clarke ; Orna Grumberg ; Doron A. Peled
Editeur :	Cambridge, Mass. : MIT Press
Année de publication :	1999
Importance :	1 vol. (314 p.)
Présentation :	ill.
Format :	24 cm
ISBN/ISSN/EAN :	978-0-262-03270-4
Catégories :	Informatique
Mots-clés :	Ordinateurs : Circuits : Conception et construction Structure logique Ordinateurs : Fiabilité Systèmes informatiques - Vérification Architecture des ordinateurs
Index. décimale :	004.2 Analyse, conception et évaluation des systèmes informatiques
Résumé :	La vérification de modèle est une technique de vérification de systèmes concurrents à états finis tels que des conceptions de circuits séquentiels et des protocoles de communication. Il présente un certain nombre d'avantages par rapport aux approches traditionnelles basées sur la simulation, les tests et le raisonnement déductif. En particulier, la vérification du modèle est automatique et généralement assez rapide. De plus, si la conception contient une erreur, la vérification du modèle produira un contre-exemple qui pourra être utilisé pour localiser la source de l'erreur. La méthode, récompensée par le Prix ACM Paris Kanellakis de 1998 pour la théorie et la pratique, a été utilisée avec succès dans la pratique pour vérifier de véritables dessins industriels, et les entreprises commencent à commercialiser des vérificateurs de modèles commerciaux. Le principal défi dans la vérification de modèle est de traiter le problème d'explosion d'espace d'état. Ce problème se produit dans les systèmes avec de nombreux composants qui peuvent interagir entre eux ou avec des structures de données pouvant prendre plusieurs valeurs différentes. Dans de tels cas, le nombre d'états globaux peut être intense. Les chercheurs ont fait des progrès considérables sur ce problème au cours des dix dernières années. C'est la première présentation complète de la théorie et de la pratique de la vérification des modèles. Le livre, qui comprend des techniques, des algorithmes et des outils basiques et de pointe, peut être utilisé à la fois comme introduction au sujet et comme référence pour les chercheurs.
Note de contenu :	Sommaire Preface 1 Introduction 1.1 The Need for Formal Methods 1.2 Hardware and Software Verification 1.3 The Process of Model Checking 1.4 Temporal Logic and Model Checking 1.5 Symbolic Algorithms 1.6 Partial Order Reduction 1.7 Other Approaches to the State EXplosion Problem 2 Modeling Systems 2.1 Modeling Concurrent Systems 2.2 Concurrent Systems 2.3 EXample of Program Translation 3 Temporal Logics 3.1 The Computation Tree Logic CTL* 3.2 CTL and LTL 3.3 Fairness 4 Model Checking 4.1 CTL Model Checking 4.2 LTL Model Checking by Tableau 4.3 CTL* Model Checking 5 Binary Decision Diagram 5.1 Representing Boolean Formulas 5.2 Representing Kripke Structures 6 Symbolic Model Checking 6.1 FiXpoint Representations 6.2 Symbolic Model Checking for CTL 6.3 Fairness in Symbolic Model Checking 6.4 CountereXamples and Witnesses 6.5 An ALU EXample 6.6 Relational Product Computations 6.7 Symbolic LTL Model Checking 7 Model Checking for the µCalculus 7.1 Introduction 7.2 The Propositional µCalculus 7.3 Evaluating FiXpoint Formulas 7.4 Representing µCalculus Formulas Using OBDDs 7.5 Translating CTL into the µCalculus 7.6 CompleXity Considerations 8 Model Checking in Practice 8.1 The SMV Model Checker 8.2 A Realistic EXample 9 Model Checking and Automata Theory 9.1 Automata on Finite and Infinite Words 9.2 Model Checking Using Automata 9.3 Checking Emptiness 9.4 Translating LTL into Automata 9.5 OntheFly Model Checking 9.6 Checking Language Containment Symbolically 10 Partial OrderReduction 10.1 Concurrency in Asynchronous Systems 10.2 Independence and Invisibility 10.3 Partial Order Reduction for LTLX 10.4 An EXample 10.5 Calculating Ample Sets 10.6 Correctness of the Algorithm 10.7 Partial Order Reduction in SPIN 11 Equivalences and Preorders between Structures 11.1 Equivalence and Preorder Algorithms 11.2 Tableau Construction 12 Compositional Reasoning 12.1 Composition of Structures 12.2 Justifying AssumeGuarantee Proofs 12.3 Verifying a CPU Controller 13 Abstraction 13.1 Cone of Influence Reduction 13.2 Data Abstraction 14 Symmetry 14.1 Groups and Symmetry 14.2 Quotient Models 14.3 Model Checking with Symmetry 14.4 CompleXity Issues 14.5 Empirical Results 15 Infinite Families of FiniteState Systems 15.1 Temporal Logic for Infinite Families 15.2 Invariants 15.3 Futurebus+ EXample Reconsidered 15.4 Graph and Network Grammars 15.5 Undecidability Result for a Family of Token Rings 16 Discrete RealTime and Quantitative Temporal Analysis 16.1 RealTime Systems and RateMonotonic Scheduling 16.2 Model Checking RealTime Systems 16.3 RTCTL Model Checking 16.4 Quantitative Temporal Analysis: Minimum/MaXimum Delay 16.5 EXample: An Aircraft Controller 17 Continuous Real Time 17.1 Timed Automata 17.2 Parallel Composition 17.3 Modeling with Timed Automata 17.4 Clock Regions 17.5 Clock Zones 17.6 Difference Bound Matrices 17.7 CompleXity Considerations 18 Conclusion References IndeX
Côte titre :	Fs/19798

Model checking [texte imprimé] / E. M. Clarke ; Orna Grumberg ; Doron A. Peled . - Cambridge, Mass. : MIT Press, 1999 . - 1 vol. (314 p.) : ill. ; 24 cm.
ISBN : 978-0-262-03270-4

Catégories :	Informatique
Mots-clés :	Ordinateurs : Circuits : Conception et construction Structure logique Ordinateurs : Fiabilité Systèmes informatiques - Vérification Architecture des ordinateurs
Index. décimale :	004.2 Analyse, conception et évaluation des systèmes informatiques
Résumé :	La vérification de modèle est une technique de vérification de systèmes concurrents à états finis tels que des conceptions de circuits séquentiels et des protocoles de communication. Il présente un certain nombre d'avantages par rapport aux approches traditionnelles basées sur la simulation, les tests et le raisonnement déductif. En particulier, la vérification du modèle est automatique et généralement assez rapide. De plus, si la conception contient une erreur, la vérification du modèle produira un contre-exemple qui pourra être utilisé pour localiser la source de l'erreur. La méthode, récompensée par le Prix ACM Paris Kanellakis de 1998 pour la théorie et la pratique, a été utilisée avec succès dans la pratique pour vérifier de véritables dessins industriels, et les entreprises commencent à commercialiser des vérificateurs de modèles commerciaux. Le principal défi dans la vérification de modèle est de traiter le problème d'explosion d'espace d'état. Ce problème se produit dans les systèmes avec de nombreux composants qui peuvent interagir entre eux ou avec des structures de données pouvant prendre plusieurs valeurs différentes. Dans de tels cas, le nombre d'états globaux peut être intense. Les chercheurs ont fait des progrès considérables sur ce problème au cours des dix dernières années. C'est la première présentation complète de la théorie et de la pratique de la vérification des modèles. Le livre, qui comprend des techniques, des algorithmes et des outils basiques et de pointe, peut être utilisé à la fois comme introduction au sujet et comme référence pour les chercheurs.
Note de contenu :	Sommaire Preface 1 Introduction 1.1 The Need for Formal Methods 1.2 Hardware and Software Verification 1.3 The Process of Model Checking 1.4 Temporal Logic and Model Checking 1.5 Symbolic Algorithms 1.6 Partial Order Reduction 1.7 Other Approaches to the State EXplosion Problem 2 Modeling Systems 2.1 Modeling Concurrent Systems 2.2 Concurrent Systems 2.3 EXample of Program Translation 3 Temporal Logics 3.1 The Computation Tree Logic CTL* 3.2 CTL and LTL 3.3 Fairness 4 Model Checking 4.1 CTL Model Checking 4.2 LTL Model Checking by Tableau 4.3 CTL* Model Checking 5 Binary Decision Diagram 5.1 Representing Boolean Formulas 5.2 Representing Kripke Structures 6 Symbolic Model Checking 6.1 FiXpoint Representations 6.2 Symbolic Model Checking for CTL 6.3 Fairness in Symbolic Model Checking 6.4 CountereXamples and Witnesses 6.5 An ALU EXample 6.6 Relational Product Computations 6.7 Symbolic LTL Model Checking 7 Model Checking for the µCalculus 7.1 Introduction 7.2 The Propositional µCalculus 7.3 Evaluating FiXpoint Formulas 7.4 Representing µCalculus Formulas Using OBDDs 7.5 Translating CTL into the µCalculus 7.6 CompleXity Considerations 8 Model Checking in Practice 8.1 The SMV Model Checker 8.2 A Realistic EXample 9 Model Checking and Automata Theory 9.1 Automata on Finite and Infinite Words 9.2 Model Checking Using Automata 9.3 Checking Emptiness 9.4 Translating LTL into Automata 9.5 OntheFly Model Checking 9.6 Checking Language Containment Symbolically 10 Partial OrderReduction 10.1 Concurrency in Asynchronous Systems 10.2 Independence and Invisibility 10.3 Partial Order Reduction for LTLX 10.4 An EXample 10.5 Calculating Ample Sets 10.6 Correctness of the Algorithm 10.7 Partial Order Reduction in SPIN 11 Equivalences and Preorders between Structures 11.1 Equivalence and Preorder Algorithms 11.2 Tableau Construction 12 Compositional Reasoning 12.1 Composition of Structures 12.2 Justifying AssumeGuarantee Proofs 12.3 Verifying a CPU Controller 13 Abstraction 13.1 Cone of Influence Reduction 13.2 Data Abstraction 14 Symmetry 14.1 Groups and Symmetry 14.2 Quotient Models 14.3 Model Checking with Symmetry 14.4 CompleXity Issues 14.5 Empirical Results 15 Infinite Families of FiniteState Systems 15.1 Temporal Logic for Infinite Families 15.2 Invariants 15.3 Futurebus+ EXample Reconsidered 15.4 Graph and Network Grammars 15.5 Undecidability Result for a Family of Token Rings 16 Discrete RealTime and Quantitative Temporal Analysis 16.1 RealTime Systems and RateMonotonic Scheduling 16.2 Model Checking RealTime Systems 16.3 RTCTL Model Checking 16.4 Quantitative Temporal Analysis: Minimum/MaXimum Delay 16.5 EXample: An Aircraft Controller 17 Continuous Real Time 17.1 Timed Automata 17.2 Parallel Composition 17.3 Modeling with Timed Automata 17.4 Clock Regions 17.5 Clock Zones 17.6 Difference Bound Matrices 17.7 CompleXity Considerations 18 Conclusion References IndeX
Côte titre :	Fs/19798