Issue No.09 - September (1990 vol.16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.58782
<p>A formal method for decomposing the critical requirements of a system into requirements of its component processes and a minimal, possibly empty, set of synchronization requirements is described. The trace model of Hoare's communicating sequential processes (CSP) is the basis for the formal method. The method is applied to an abstract voice transmitter and describes the role that the EHDM verification system plays in the transmitter's decomposition is described. In combination with other verification techniques, it is expected that this method will promote the development of more trustworthy systems.</p>
specification; verified decomposition; system requirements; CSP; formal method; synchronization requirements; trace model; formal specification; synchronisation; theorem proving.
A.P. Moore, "The Specification and Verified Decomposition of System Requirements Using CSP", IEEE Transactions on Software Engineering, vol.16, no. 9, pp. 932-948, September 1990, doi:10.1109/32.58782