On the Use of Formal Specifications to Analyze Fault Behaviors of Distributed Systems

摘要

The development of distributed systems is considered a complex task. The process of assuring the correctness of such systems is even more difficult if we consider open environments (e.g. Internet), where faults may occur. To help such process we make use of formal methods and tools as means to specify and reason about the behavior of distributed systems in the presence of faults. We use a graphical and declarative formal specification language, called Object Based Graph Grammars, to model asynchronous distributed systems. The approach used to specify and analyze the behavior of distributed systems in the presence of faults is based on the observation that a fault behavior can be modeled as an unwanted but possible state transition of a system. Following this approach we can define a fault model, like crash for example, as being a transformation of a model. Thus, a model M_1 of a distributed system can be transformed into a model M_2, that comprehends the behavior of some kind of fault model. To show these methods and tools we model a pull-based failure detector as a case study.