Guaranteeing recoverability in electronic commerce

Electronic commerce systems (retail, auction, etc.) are good examples of data-based systems that operate under correctness and resilience requirements of a transactional nature but go beyond conventional databases, as they are formed by the aggregation of heterogeneous, autonomous components. We introduce a framework to specify, analyze and reason about the behavior of such systems, focusing on how they are designed to make consistent progress in spite of failures. The contributions are: (a) the introduction of the Guarantee abstraction to deal with transactional applications; (b) a framework based on guarantees and protocols to specify the behaviors of systems and their components and reason about the properties of systems and their components; and (c) application of the framework to a common e-commerce scenario. The framework allows the hierarchical composition of transactional systems and their properties, as well as the proofs of these properties: we specify a system´s behavior at its most abstract level, and proceed to decompose the specification mirroring the structure of the system´s components, considering the role of guarantee-preserving component systems and recovery in each case. In particular we show how the lower-level properties are supported by the component systems, which we also characterize within the same framework