Search

Formal refinement shows how the specification of a program can be transformed by steps into an executable implementation. The method is sound and rigorous but is not suited to dealing with large and complex programs. Thus, the construction of large programs is often assumed to remain outside the scope of formal representation altogether and informal techniques, sometimes using diagrammatic notations, are used to go from requirements to programs. In this paper, we show how large programs can be defined in terms of different views that are instances of a single meta model. Each view represents one set of properties of the program and their composition defines the specification of the program. Transformations are used to convert views into program fragments that are composed together to build the whole program. The technique has been applied for the construction of many large systems that are in practical use.

The incorporation of a recovery algorithm into a program can be viewed as a program transformation, converting the basic program into a fault-tolerant version. We present a framework in which such program transformations are accompanied by a corresponding formula transformation which obtains properties of the fault-tolerant versions of the programs from properties of the basic programs. Compositionality is achieved when every property of the fault-tolerant version can be obtained from a transformed property of the basic program. A verification method for proving the correctness of formula transformations is presented. This makes it possible to prove just once that a formula transformation corresponds to a program transformation, removing the need to prove separately the correctness of each transformed program. Keywords: Parallel Algorithms, Distributed Algorithms, Fault-Tolerance, Specification, Verification.

Proving that a real-time system is capable of handling a peak processing load is a difficult problem, especially when a large number of devices are connected at different priority levels. In this paper we first provide a good solution for the case where the maximum frequency of inputs from each device and the maximum processing times for each input are both known. This is then used to estimate response times and to deal with buffered computation.