Verifying fault-tolerant distributed systems using object-based graph grammars
F. L. Dotti, O. Mendizabal and O. M. Santos
Assuring the correctness of fault-tolerant distributed systems can be an overwhelming task. Besides dealing with complex problems of distributed systems, it is also necessary to design the system in such a way that a well-defined failure behaviour, or the masking of failure components, is presented by the system when components fail. To help reasoning about such systems, the use of formal methods becomes desirable. In previous work we introduced a graphical formal specification language, called Object-Based Graph Grammars (OBGG), for modelling asynchronous distributed systems. We also defined a method for automatically inserting classical fault behaviours into OBGG models. The obtained models could be analysed using simulation. In this paper a new method for automatically inserting fault behaviours into OBGG models, which is suitable for using verification as the analysis method, is proposed. Moreover, we show how to formally verify OBGG models in the presence of such faults. A two phase commit protocol is used to illustrate the contributions.
Download Not Available
BibTex Entry
@inproceedings{Dotti2005,
author = {F. L. Dotti and O. Mendizabal and O. M. Santos},
booktitle = {Dependable Computing: Second Latin-American Symposium, LADC},
pages = {80--100},
publisher = {Springer-Verlag},
title = {Verifying fault-tolerant distributed systems using object-based graph grammars},
volume = {LNCS 3747},
year = {2005}
}