Abstract
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.
This work is partially sponsored by IQ-MObile (CNPq/CNR) and DACHIA (FAPERGS/IB-BMBF) projects. Authors appear in alphabetical order.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Birman, K.P.: Building secure and reliable network applications. Manning Publications, USA (1996)
Burch, J.R., et al.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)
Chechik, M., Păun, D.O.: Events in property patterns. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 154–167. Springer, Heidelberg (1999)
Cristian, F.: A rigorous approach to fault-tolerant programming. IEEE Trans. on Soft. Eng. 11(1), 23–31 (1985)
Cristian, F.: Understanding fault-tolerant distributed systems. Communications of the ACM 34(2), 56–78 (1991)
Dotti, F.L., Duarte, L.M., Copstein, B., Ribeiro, L.: Simulation of mobile applications. In: 2002 Communication Networks and Distributed Systems Modeling and Simulation Conference, USA, pp. 261–267. SCS (2002)
Dotti, F.L., et al.: An environment for the development of concurrent object-based applications. Eletronic Notes in Theoretical Computer Science 127, 3–13 (2005)
Dotti, F.L., Foss, L., Ribeiro, L., Santos, O.M.: Verification of object-based distributed systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 261–275. Springer, Heidelberg (2003)
Dotti, F.L., Ribeiro, L.: Specification of mobile code systems using graph grammars. In: 4th Int. Conference on Formal Methods for Open Object-Based Distributed Systems, IFIP Conference Proceedings, USA, vol. 177, pp. 45–64. Kluwer Academic Publishers, Dordrecht (2000)
Dotti, F.L., Santos, O.M., Rödel, E.T.: On the use of formal specifications to analyze fault behaviors of distributed systems. In: de Lemos, R., Weber, T.S., Camargo Jr., J.B. (eds.) LADC 2003. LNCS, vol. 2847, pp. 341–360. Springer, Heidelberg (2003)
Fournet, C., et al.: A calculus of mobile agents. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 406–421. Springer, Heidelberg (1996)
Gärtner, F.C.: Specification for fault tolerance: a comedy of failures. Technical Report TUD-BS-1998-03, Department of Computer Science - Darmstadt University of Technology, Germany (1998)
Gärtner, F.C.: Fundamentals of fault-tolerant distributed computing in asynchronous environments. ACM Computing Surveys 31(1), 1–26 (1999)
Hadzilacos, V., Toueg, S.: A modular approach to fault-tolerant broadcasts and related problems. Technical Report TR94-1425, Department of Computer Science, Cornell University, USA (1994)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Soft. Eng. 23(5), 279–295 (1997)
Jalote, P.: Fault tolerance in distributed systems. Prentice Hall, USA (1994)
Lamport, L., Lynch, N.: Distributed computing: models and methods. In: Handbook of theoretical computer science, vol. B. formal models and semantics, Elsevier, Amsterdam (1990)
Lynch, N.A.: Distributed algorithms. Morgan Kaufmann, USA (1996)
Perraju, T.S., Rana, S.P., Sarkar, S.P.: Specifying fault tolerance in mission critical systems. In: 1st IEEE High Assurance Systems Engineering Workshop, Canada, pp. 24–31. IEEE Computer Society Press, Los Alamitos (1996)
Perry, K.J., Toueg, S.: Distributed agreement in the presence of processor and communication faults. IEEE Trans. on Soft. Eng. 12(3), 477–482 (1986)
Rensink, A., Schmidt, Á., Varró, D.: Model checking graph transformations: a comparison of two approaches. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 226–241. Springer, Heidelberg (2004)
Rozenberg, G. (ed.): Handbook of graph grammars and computing by graph transformation, Foundations, vol. 1. World Scientific Publisher, Singapore (1997)
Santos, O.M., Dotti, F.L., Ribeiro, L.: Verifying object-based graph grammars. Eletronic Notes in Theoretical Computer Science 109, 125–136 (2004)
Yokogawa, T., Tsuchiya, T., Kikuno, T.: Automatic verification of fault tolerance using model checking. In: 2001 Pacific Rim Int. Symposium on Dependable Computing, Korea, pp. 95–102. IEEE Computer Society Press, Los Alamitos (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dotti, F.L., Mendizabal, O.M., dos Santos, O.M. (2005). Verifying Fault-Tolerant Distributed Systems Using Object-Based Graph Grammars. In: Maziero, C.A., Gabriel Silva, J., Andrade, A.M.S., de Assis Silva, F.M. (eds) Dependable Computing. LADC 2005. Lecture Notes in Computer Science, vol 3747. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11572329_9
Download citation
DOI: https://doi.org/10.1007/11572329_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29572-3
Online ISBN: 978-3-540-32092-0
eBook Packages: Computer ScienceComputer Science (R0)