Formal Verification of a Transactional Interaction Contract

A transactional information system guarantees as part of the ACID contract that multiple operations pertaining to a transaction are executed atomically and that if completed their effect is durable. However, message losses resulting from client and server crashes are not part of the transaction. Unlike failures occurring in the midst of a transaction (leading to its abort), the loss of a reply to the final commit message poses a problem of determining the transaction outcome that cannot be solved generically using state-of-the-art OLTP systems. This paper develops a formal specification of a generic transactional interaction contract that is part of a broader Interaction Contracts framework guaranteeing the exactly-once execution in general multi-tier applications. The formal specification is designed and verified using the statechart language and model checking in the reactive system design tool called Statemate.