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

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