| Summary: | Reversible debuggers help programmers to find the causes of misbehaviours in
concurrent programs more quickly, by executing a program backwards from the
point where a misbehaviour was observed, and looking for the bug(s) that caused
it. Reversible debuggers can be founded on the well-studied theory of
causal-consistent reversibility, which only allows one to undo an action
provided that its consequences, if any, are undone beforehand.
Causal-consistent reversibility yields more efficient debugging by reducing the
number of states to be explored when looking backwards. Till now,
causal-consistent reversibility has never considered time, which is a key
aspect in real-world applications. Here, we study the interplay between
reversibility and time in concurrent systems via a process algebra. The
Temporal Process Language (TPL) by Hennessy and Regan is a well-understood
extension of CCS with discrete-time and a timeout operator. We define revTPL, a
reversible extension of TPL, and we show that it satisfies the properties
expected from a causal-consistent reversible calculus. We show that,
alternatively, revTPL can be interpreted as an extension of reversible CCS with
time.
|
|---|