Issue No. 05 - May (1993 vol. 19)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.232015
<p>The formal derivation of an implementation of the I/O (input/output) subsystem portion of an existing operating system is presented. The I/O subsystem is responsible for allocating I/O resources such as tapes, disks, I/O channels in response to requests from user processes. The derivation employs the UNITY methodology which captures the concurrent interaction of the I/O subsystem with its environment. The verified resource allocation algorithm that results from the derivation has been used as part of a high-level design by software engineers implementing the I/O subsystem. As the largest application to date of the UNITY methodology, the derivation illustrates a number of techniques for organizing large specifications and proofs.</p>
formal derivation; I/O subsystem; concurrent programs; operating system; tapes; disks; I/O channels; UNITY methodology; resource allocation algorithm; specifications; proofs; formal specification; parallel programming; program verification
M. Staskauskas, "Formal Derivation of Concurrent Programs: An Example from Industry," in IEEE Transactions on Software Engineering, vol. 19, no. , pp. 503-528, 1993.