Title :
Formal Modeling and Analysis of a Distributed Database Protocol in Maude
Author_Institution :
Dept. of Inf., Oslo Univ., Oslo
Abstract :
This paper illustrates how the rewriting-logic-based Maude tool, and its extension real-time Maude, can be applied to the formal object-oriented specification, simulation, and model checking of the two-phase commit protocol for distributed databases. Maude´s intuitive yet expressive specification language, its support for object-oriented formal specification, its high-performance formal analysis features, and its track record should make it a promising candidate to successfully analyze advanced state-of-the-art distributed database protocols.
Keywords :
distributed databases; formal specification; protocols; distributed database protocol; expressive specification language; extension real-time Maude; formal modeling; formal object-oriented specification; high-performance formal analysis features; two-phase commit protocol; Algorithm design and analysis; Analytical models; Distributed databases; Equations; Formal specifications; Object oriented databases; Object oriented modeling; Protocols; Spatial databases; State-space methods; distributed databases; formal modeling; model checking; rewriting logic; transaction protocols;
Conference_Titel :
Computational Science and Engineering Workshops, 2008. CSEWORKSHOPS '08. 11th IEEE International Conference on
Conference_Location :
San Paulo
Print_ISBN :
978-0-7695-3257-8
DOI :
10.1109/CSEW.2008.30
