Design and verification of long-running transactions in a timed framework