Showing Correctness of a Replication Algorithm in a Component based System.

H. Wu, B. Kemme

Reasoning about the correctness of a replication algorithm is a difficult endeavor. If correctness has to be shown for a component based architecture where a client request can lead to execution across different components or tiers, this is even more difficult. Existing formalisms are either restricted to systems with only one component, or make strong assumptions about the setup of the system. In this paper, we present a flexible framework to reason about exactly-once execution in a failure-prone replicated component based system. Our approach allows us to reason about the execution across the entire system, e.g., application server and database tier. If a given replication algorithm makes assumptions about some of the components, then those can be easily integrated into the reasoning process.
IDEAS Conf., September 2008.