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 address 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 transactions. Formal specification and reasoning for transaction properties have been limited to proof-theoretic approaches, despite the recent progress in model checking. In this work, we present a model-driven approach for generating a provably correct implementation of the transaction model of interest. The model is specified by state machines for the transaction participants, which are synchronized on a set of events. All possible execution paths of the synchronized state machines are checked for property violations. An implementation for the verified transaction model is then automatically generated. To demonstrate the approach, the specification of nested transactions is verified, because it is the basis for many advanced transaction models. Concurrency and Computation: Practice and Experience.