Using eternity variables to specify and prove a serializable database interface

Eternity variables are introduced to specify and verify serializability of transactions of a distributed database. Eternity variables are a new kind of auxiliary variables. They do not occur in the implementation but are used in specification and verification. Elsewhere it has been proved that eternity variables in combination with history variables are semantically complete for proving refinement relations. An eternity variable can be thought of as an unknown constant that is determined by the behaviour (execution sequence). In the specification of the database, one eternity variable is used to enforce serialization. In the verification, an additional eternity variable is needed for the connection of the local data with the shared database. The formalism is based on linear-time temporal logic, but the analysis of behaviours is completely reduced to the next-state relation together with progress arguments using variant functions. Forward invariants (inductive predicates) are complemented with other, so-called backward, invariants. The proof has been verified with the first-order theorem prover NQTHM to give additional confidence in the result and in the feasibility of the approach.