The formal specification and design of a distributed electronic funds-transfer system

Abstract

The design of an electronic funds-transfer (EFT) system, using the UNITY parallel programming methodology, is presented. The process begins with a high-level specification that captures the essence of transaction processing in the system. In a series of refinement steps, this specification is transformed into one that leads directly to a program suitable for execution on the distributed architecture of the EFT system. Each refinement step involves replacing a data structure by a distributed version that can be implemented efficiently on the target architecture. By defining a correspondence between the replaced data structure and its distributed counterpart, it can be demonstrated formally that each refinement step preserves the intent of the original specification.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>