ABSTRACT
The designer of a distributed system has the responsibility of certifying the correctness of the system, before users start using it. This guarantee must hold as long as every hardware and software component works according to specifications. A system may function incorrectly when its components fail, or the process states are corrupted by external perturbations and there is no provision for faulttolerance, or there is a design flow. This chapter explains what correctness criteria are considered important for distributed systems and how to prove these correctness properties.
