The ACID model checker and code generator for transaction processing

Traditional transaction processing aims in delivering the ACID properties (Atomicity, Consistency, Isolation, Durability), that in our days are often relaxed, due to the need for transaction models that suit modern computing environments and workflow management applications. Typical examples are the requirements of long-running transactions in mobile computing or in the web, as well as the requirements of business-to-business collaborative applications. However, there is lack of tools for automatically verifying correctness of transaction model implementations. This work presents the ACID model checker and code generator, which plays a vital role in developing correct simulation models for the ACID Sim Tools environment. In essence, our contribution introduces an approach for automatically generating provably correct implementations of transaction management, for the transaction model of interest.