A formal method for providing temporal equivalence in binary-to-binary translation of real-time applications

Presents a formal method to provide temporal equivalence in binary-to-binary translation of real-time applications. We first define three different levels of temporal equivalence, i.e. timing equivalence, invariance and divergence. We then find necessary and sufficient conditions for these three levels of temporal equivalence. We take an interval-based approach to test these conditions. If the generated target program is executable with timing equivalence or invariance, it has to be enforced to do so by inserting synchronization. Synchronization methods that enforce the temporal equivalence are also presented