Models and Analysis for Distributed Systems

Book Preface

Verification and hence modeling are a mandatory but intricate problem for engineers developing embedded distributed real-time systems that are entrusted with critical safety applications like medical care, transportation, energy production, industrial processes, military operations. Therefore, while emerging 40 years ago, first for circuit design, avionics and finally for all domains, verification environments are now widely exploited by industry and fully integrated into the development processes.

Volume 1 presented design and algorithms for developing these large-scale distributed systems, real-time embedded ones, security concepts for peer-to-peer and ubiquitous computing. However the crucial problem of their correctness is made hard by their complexity, the difficulty of managing fault tolerance, the real-time constraints that they must satisfy, asynchronism of worldly spread units as well as the heterogeneity of devices, networks and applications.

This second volume presents different approaches for mastering these verification problems, beginning with the main concepts and formal methods used for modeling and well structuring distributed systems and for expressing their logical and timed properties. Then it explores the theoretical approaches, mainly logic and automata theory, for behavioral verification of these models. It goes thoroughly into the decidability issues and algorithmic complexity that are the inherent obstacles to overcome particularly for dealing with infinite state spaces and timed models. Collecting the experience of researchers from several laboratories, this volume covers advanced topics of distributed system modeling and verification. It aims at giving a deep knowledge of theory, methods and algorithms to Masters and PhD students as well as to engineers who are already good experts in verification.