Architecture-Directed Refinement
Abstract
As critical computer systems continue to grow in complexity, the task of demonstrating that they are correct, that is, guaranteed to operate without failure, becomes more difficult. For this reason, research in software engineering has turned to formal methods, i.e. rigorous approaches to demonstrating the correctness of software systems. Unfortunately, the formal methods currently used for concurrent systems do no provide a mechanism for expressing and manipulating non-functional constraints formally. In this paper, we show that one class of non-functional constraints, the target architectures, can be expressed using formal notation (the UNITY proof logic). We then use a mixture of specifications and program refinements to derive a program which is demonstrably correct, both functionally and in its appropriateness for implementation on a specific machine.