Showing Correctness of a Replication Algorithm in a Component based System.
H. Wu, B. Kemme
Abstract:
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.