Transaction management is an essential component of database management systems. It enables multiple users to access the database concurrently while preserving transactional properties such as atomicity, consistency, isolation, and durability. In this paper, we propose a formal framework specification for transaction processing. Our work can be seen as an extension of previous work by Gurevich et al. who have presented a formalism for general database recovery processing. Based on this formalism, we incorporate additional mechanisms that remove several explicit constraints, support normal transaction processing, and, most importantly, apply the approach to more advanced recovery mechanisms.

transaction processing, concurrency control, database recovery, Abstract State Machines