Design and Verification of Long-Running Transactions in a Timed Framework