In this book we develop powerful techniques based on formal methods for
the verification of correctness, consistency and safety properties
related to dynamic reconfiguration and communication in complex
distributed systems. In particular, static analysis techniques based on
types and type systems are an adequate methodology considering their
success in guaranteeing not only basic safety properties, but also more
sophisticated ones like deadlock or lock freedom in concurrent
settings.The main contributions of this book are twofold.
i) We design a type system for a concurrent object-oriented calculus to
statically ensure consistency of dynamic reconfigurations.
ii) We define an encoding of the session pi-calculus, which models
communication in distributed systems, into the standard typed
pi-calculus. We use this encoding to derive properties like type safety
and progress in the session pi-calculus by exploiting the corresponding
properties in the standard typed pi-calculus.