This theory is developed in the paper Eternity Variables to Prove Simulation of Specifications ACM-ToCL 6 (2005) 1-27. Almost all of it has been verified with a proof script for the theorem prover PVS.
The theory is applied to the serializable database
interface problem of Distributed Computing 6 (1992). This work is
described in
Eternity variables to specify and prove a serializable database
interface, Science of Computer Programming
51 (2004) 47--85.
The mechanical
proof was done with
NQTHM, based on my
prelude for concurrency.
The completeness result has been simplified and extended in Universal extensions to simulate specifications, Information and Computation 206 (2008) 108-128. This has been verified with a proof script in PVS.
A simpler application of eternity variables as well as the development of gliding simulations is in the paper A Criterion for Atomicity Revisited. The PVS proof script has been revised (Oct. 2007) to accomodate the next application.
This revised criterion for atomicity has been applied to prove algorithm C2 of Haldar and Vidyasankar in A challenge for atomicity verification, Science of Computer Programming 71 (2008) 57-72, with refinement functions and forward simulations, and verified with PVS.
In "Simulation refinement for concurrency verification" (2009) we introduced episodic simulations with application to Lipton's mutual exclusion theory and mutex abstraction in (e.g.) pthreads. This is also verified with PVS.