Transformational design of a fault tolerant sequential memory component

A sequential memory component stores and retrieves data in addressable locations. A fault tolerant implementation suspends read commands to locations without a prior assignment until data becomes available at the requested location. The paper studies the systematic top-down design of a fault tolerant sequential memory component in the setting of stream functions and state transition machines. We formally refine the communication-oriented input/output behaviour into a state-based implementation. The transformation employs a history abstraction function which extracts the component's internal state from the input history. Beyond the particular case study, we explicate generally applicable formal methods for the functional specification and systematic design of interactive components in distributed systems with asynchronous communication.