Formal Specification of Fault Tolerant Distributed Systems in the Action Systems Formalism

Ensuring dependability of distributed systems is a complex task. Since distributed systems are usually large, testing and state-exploring approaches are often inadequate for guarantying high degree of dependability. In this paper, we propose a formal scalable approach to specifying and verifying fault tolerant distributed systems. The approach is based on the action systems formalism and stepwise refinement. Application of the proposed approach allows us to achieve correct implementation of fault tolerance mechanisms in large distributed systems.