The Specification and Verified Decomposition of System Requirements Using CSP
NAVAL RESEARCH LAB WASHINGTON DC
Pagination or Media Count:
An important principle of building trustworthy systems is to rigorously analyze the critical requirements early in the development process, even before starting system design. Existing proof methods for systems of communicating processes focus on the bottom-up composition of component-level specifications into system-level specifications. Trustworthy system development requires, instead, the top-down derivation of component requirements from the critical system requirements. This paper describes a formal method for decomposing the requirements of a system into requirements of its component processes and a minimal, possibly empty, set of synchronization requirements. The Trace Model of Hoares Communicating Sequential Processes CSP is the basis for the formal method. We apply the method to an abstract voice transmitter and describe the role that the EHDM verification system plays in the transmitters decomposition. In combination with other verification techniques, we expect that the method defined here will promote the development of more trustworthy systems.
- Computer Programming and Software