On Deriving Distributed Programs from Formal Specifications of Functional Requirements and Architectural Constraints

Authors

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

Document Type

Technical Report

Publication Date

1992-03-01

Filename

WUCS-91-05.pdf

Technical Report Number

WUCS-91-05

Abstract

This design of distributed programs is a difficult task which can greatly benefit from the application of formal methods. Since design solutions are determined not only by functional requirements imposed by the application but also by the structure and behavior of the underlying hardware architecture, a complete formal treatment of the program derivation process becomes a significant challenge. The common approach is to state with a formal specification of the functional requirements and to derive the desired program through systematic refinements which factor in the architectural constraints informally, in an ad-hoc manner. This paper shows how one can employ a single specification method (program0wide assertions) to express both functional requirements and architectural constraints. A distributed simulation problem is used to illustrate a formal strategy for deriving a distributed program from assertions about its functionality and the constraints imposed by the choice of underlying architecture.

Comments

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

Recommended Citation

Roman, Gruia-Catalin; Wilcox, C. Donald; and Plum, Jerome Y., "On Deriving Distributed Programs from Formal Specifications of Functional Requirements and Architectural Constraints" Report Number: WUCS-91-05 (1992). All Computer Science and Engineering Research.
https://openscholarship.wustl.edu/cse_research/623