Correctness proof of a database replication protocol under the perspective of the I/O automaton model | Publicación