The Community for Technology Leaders
Green Image
<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.G. Staskauskas, "Formal Derivation of Concurrent Programs: An Example from Industry", IEEE Transactions on Software Engineering, vol. 19, no. , pp. 503-528, May 1993, doi:10.1109/32.232015
92 ms
(Ver 3.1 (10032016))