| Autor: |
Maziero, Carlos Alberto, Silva, João Gabriel, Andrade, Aline Maria Santos, Assis Silva, Flávio Morais de, Dotti, Fernando L., Mendizabal, Odorico M., Santos, Osmar M. |
| Zdroj: |
Dependable Computing; 2005, p80-100, 21p |
| Abstrakt: |
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. Keywords: Object-based graph grammars, distributed systems, fault-tolerance, model transformation, model checking. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Supplemental Index |
| Externí odkaz: |
|
