The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - May (1993 vol.19)
pp: 503-528
ABSTRACT
<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>
INDEX TERMS
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
CITATION
M.G. Staskauskas, "Formal Derivation of Concurrent Programs: An Example from Industry", IEEE Transactions on Software Engineering, vol.19, no. 5, pp. 503-528, May 1993, doi:10.1109/32.232015
19 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool