A Functional Solution to the RPC-Memory Specification Problem.
Manfred Broy · 1994
. We give a functional specification of the syntactic interface and the black box behavior of an unreliable and a reliable memory component and a remote procedure (RPC) call component. The RPC component controls the access to the memory. In addition, we specify a clerk for driving the RPC component. The used method is modular and therefore it allows us to specify each of these components independently and separately. We discuss the specifications shortly and then compose them into a distributed system of interacting components. We prove that the specification of the composed system fulfills again the requirement specification of the unreliable memory component. Finally we give a timed version of the RPC component and of a clerk component and compose them. 1 Introduction For describing the behavior of a reactive component we can either use state transition models or communication/action history based models. Using states, we specify the behavior of a system by a state machine that mode...