Models and Analysis for Distributed Systems

by Haddad, Serge; Kordon, Fabrice; Pautet, Laurent; Petrucci, Laure

• ISBN13: 9781848213142
• ISBN10: 184821314X
• Edition: 1st
• Format: Hardcover
• Copyright: 2011-07-12
• Publisher: Wiley-ISTE

Summary

This book presents distributed systems from a designer's point-of-view. First, it gives examples of systems taken from industrial case studies. Then, it suggests how to model them from system requirements, keeping in mind formal analysis to enforce their accuracy.

Author Biography

Serge Haddad is a full professor at Ecole Normale Suprieure de Cachan, France. His research is mainly concerned with verification of complex systems including multiple features like non-determinism, concurrency, distribution, time and probability. Fabrice Kordon is a full professor at UPMC, Paris, France. He is the head of the MoVe (Modeling and Verification) team at the CNRS Laboratoire d'Informatique de Paris 6. His research mainly concerns the modeling of complex distributed systems to enable both formal analysis and automatic program generation. Laurent Pautet is a full professor at Tlcom ParisTech, France. His research is mainly concerned with design and validation of distributed real-time embedded systems. Laure Petrucci is a full professor at University Paris 13, France. She is the head of the Networking and Telecommunication department at the Technology Institute. Her research is mainly focused on harnessing the complexity of systems verification, using modular approaches.

Table of Contents

Foreword	p. 9
Introduction	p. 17
Formal Models for Distributed Systems	p. 21
Introduction to Formal Models	p. 23
Motivation	p. 23
Semi-formal models	p. 24
Formal models	p. 27
After specification, verification	p. 35
Outline of Part I	p. 37
Bibliography	p. 37
Specification and Design Approaches	p. 41
Introduction	p. 41
Criteria for developing specifications	p. 42
Specification development methodologies	p. 50
Conclusion	p. 60
Bibliography	p. 60
Modeling Time	p. 63
Introduction	p. 63
Semantics of timed models	p. 65
Classical timed models	p. 68
Specification of timing requirements	p. 85
Conclusion	p. 90
Bibliography	p. 90
Architecture Description Languages	p. 97
Introduction	p. 97
Concepts	p. 100
Formal ADLs	p. 109
ADLs for actual implementation	p. 117
Conclusion	p. 130
Bibliography	p. 130
Verification Techniques for Distributed Systems	p. 135
Introduction to Verification	p. 137
Introduction	p. 137
Formal models for verification	p. 138
Expression of properties	p. 141
Verification methods	p. 144
Outline of Part 2	p. 151
Bibliography	p. 151
Verification of Finite-State Systems	p. 155
Introduction	p. 155
Petri net definition	p. 156
Structural approaches	p. 158
Formal verification by model-checking	p. 183
Classification of model-checking approaches	p. 191
Decision diagram-based approaches	p. 194
Partial order reductions	p. 203
Reductions exploiting symmetry	p. 212
Conclusion	p. 214
Bibliography	p. 215
Verification of Infinite-State Systems	p. 221
Introduction	p. 221
Counter systems	p. 225
Recursive Petri nets	p. 233
Presburger arithmetic as symbolic representation	p. 250
Concluding remarks	p. 263
Bibliography	p. 263
Verification of Timed Systems	p. 271
Introduction	p. 271
Construction of the region graph	p. 273
Handling infinite abstractions	p. 284
Robustness issues in timed systems	p. 293
Conclusion	p. 303
Bibliography	p. 303
Distributed Control	p. 307
Introduction	p. 307
Decentralized Control	p. 311
Controller synthesis for distributed systems	p. 323
Multi-player games	p. 339
Conclusion	p. 346
Bibliography	p. 346
List of Authors	p. 353
Index	p. 355
Table of Contents provided by Ingram. All Rights Reserved.