Architecture-Directed Refinement

Authors

Gruia-Catalin Roman, Washington University in St Louis
C. Donald Wilcox, Washington University in St Louis

Document Type

Technical Report

Publication Date

1992-10-01

Filename

WUCS-92-34.pdf

Technical Report Number

WUCS-92-34

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.

Comments

Permanent URL: http://dx.doi.org/10.7936/K7SQ8XRP

Recommended Citation

Roman, Gruia-Catalin and Wilcox, C. Donald, "Architecture-Directed Refinement" Report Number: WUCS-92-34 (1992). All Computer Science and Engineering Research.
https://openscholarship.wustl.edu/cse_research/597