The specification and verified decomposition of system requirements using CSP

摘要

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.