Nowadays, distributed systems are increasingly present, for publicsoftware applications as well as critical systems. softwareapplications as well as critical systems. This title andDistributed Systems: Design and Algorithms - from the sameeditors - introduce the underlying concepts, the associateddesign techniques and the related security issues.The objective of this book is to describe the state of the art ofthe formal methods for the analysis of distributed systems.Numerous issues remain open and are the topics of major researchprojects. One current research trend consists of profoundly mixingthe design, modeling, verification and implementation stages. Thisprototyping-based approach is centered around the concept of modelrefinement.This book is more specifically intended for readers that wish togain an overview of the application of formal methods in the designof distributed systems. Master's and PhD students, as well asengineers in industry, will find a global understanding of thetechniques as well as references to the most up-to-date works inthis area.

Foreword 9Claude GIRAULTChapter 1. Introduction 17Serge HADDAD, Fabrice KORDON, Laurent PAUTET and LaurePETRUCCIFIRST 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 Approaches41Christine 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 654.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 SYSTEMS135Chapter 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 Systems221Sté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 NathalieSZNAJDER10.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