Premium
Model checking and code generation for transaction processing software
Author(s) -
Mentis Anakreon,
Katsaros Panagiotis
Publication year - 2012
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
DOI - 10.1002/cpe.1876
Subject(s) - computer science , distributed transaction , atomicity , transaction processing system , nested transaction , database transaction , transaction processing , concurrency , consistency (knowledge bases) , distributed computing , model checking , serializability , online transaction processing , abstract state machines , programming language , software engineering , finite state machine , artificial intelligence
SUMMARY 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 . Copyright © 2012 John Wiley & Sons, Ltd.