Models and Analysis for Distributed Systems

Fabrice Kordon is a full-time professor at Université P. & M. Curie (UPMC). Serge Haddad is a full-time professor at école Normale Supérieure de Cachan, a member of the CNRS laboratory LSV, and a member of the INRIA team MExICo. Laurent Pautet is a full-time professor at Télécom ParisTech and a member of the CNRS laboratory LTCI. Laure Petrucci is a full-time professor at University Paris 13 in France and a member of the CNRS laboratory LIPN.

• Foreword 9Claude GIRAULTChapter 1. Introduction 17Serge HADDAD, Fabrice KORDON, Laurent PAUTET and Laure PETRUCCIFIRST PART. FORMAL MODELS FOR DISTRIBUTED SYSTEMS 21Chapter 2. Introduction to Formal Models 23Laure PETRUCCI2.1.Motivation 232.2.Semi-formalmodels 242.3.Formal models 272.4.After specification, verification 352.5. Outline of Part I 372.6.Bibliography 37Chapter 3. Specification and Design Approaches  41Christine CHOPPY and Laure PETRUCCI3.1. Introduction 413.2.Criteria for developing specifications 423.3. Specification development methodologies 503.4.Conclusion 603.5.Bibliography 60Chapter 4. Modeling Time 63Béatrice BÉRARD4.1. Introduction 634.2.Semantics of timed models 65 4.3.Classical timed models 684.4.Specification of timing requirements 854.5.Conclusion 904.6.Bibliography 90Chapter 5. Architecture Description Languages 97Pascal POIZAT and Thomas VERGNAUD5.1. Introduction 975.2.Concepts 1005.3.Formal ADLs 1095.4.ADLs for actual implementation 1175.5.Conclusion 1305.6.Bibliography 130SECOND PART. VERIFICATION TECHNIQUES FOR DISTRIBUTED SYSTEMS 135Chapter 6. Introduction to Verification 137Serge HADDAD6.1. Introduction 1376.2.Formal models for verification 1386.3.Expression of properties 1416.4. Verification methods 1446.5. Outline of Part 2 1516.6.Bibliography 151Chapter 7. Verification of Finite-State Systems 155Jean-François PRADAT-PEYRE and Yann THIERRY-MIEG7.1. Introduction 1557.2. Petri net definition 1567.3.Structural approaches 1587.4.Formal verification by model-checking 1837.5.Classification of model-checking approaches 1917.6.Decision diagram-based approaches 1947.7.Partial order reductions 2037.8. Reductions exploiting symmetry 2127.9.Conclusion 2147.10.Bibliography 215Chapter 8. Verification of Infinite-State Systems 221Stéphane DEMRI and Denis POITRENAUD8.1. Introduction 2218.2. Counter systems 2258.3.Recursive Petri nets 2338.4. Presburger arithmetic as symbolic representation 2508.5.Concludingremarks 2638.6.Bibliography 263Chapter 9. Verification of Timed Systems 271Pierre-Alain REYNIER9.1. Introduction 2719.2.Construction of the region graph 2739.3.Handling infinite abstractions 2849.4.Robustness issues in timed systems 2939.5.Conclusion 3039.6.Bibliography 303Chapter 10. Distributed Control 307Claude DUTHEILLET, Isabelle MOUNIER and Nathalie SZNAJDER10.1. Introduction 30710.2. Decentralized Control 31110.3. Controller synthesis for distributed systems 32310.4. Multi-player games 33910.5.Conclusion 34610.6.Bibliography 346List of Authors 353Index 355