Model Checking and Code Generation for Transaction Processing Software
In modern transaction processing software, the ACID properties (Atomicity, Consistency, Isolation, Durability) are often relaxed, in order to ad-dress requirements that arise in computing environments of today. Typical examples are the long-running transactions in mobile computing, in service oriented architectures and B2B collaborative applications. These new transaction models are collectively known as advanced or extended transaction. Formal specification and reasoning for transaction properties has been limited to proof-theoretic approaches, despite the recent progress in model checking.