A formal perspective to specification of transaction systems
Sylvanus A. Ehikioya, Ken Barker · South African Computer Journal · 2000
This paper describes the relationship and relevance of predicate logic in the specification of transaction system protocols.We present a formal specification technique based on concurrent execution that provides automatic communication and synchronization mechanisms between concurrent processes. This framework is not biased towards specific types of trans-actions.It integrates temporal behaviour of individual transactions with the dependencies that can arise when accessing shareable data. Our approach allows the specification of transaction constraints and transaction dependencies in a declarative fashion. This provides flexibility in their implementation and permits different techniques to enforce the constraints independent of the application program. This paper explores the issues of correctness, reliability, and recovery of data distributed across the enterprise; describes techniques for guaranteeing and enhancing correctness; and procedures for recovering transactions and data in case of any transaction failures to guarantee a high degree of system dependability.