|
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. |
