FORMAL DERIVATION OF CONCURRENT PROGRAMS - AN EXAMPLE FROM INDUSTRY

We present the formal derivation of an implementation of the I/O subsy stem portion of an existing operating system. The I/O subsystem is res ponsible for allocating I/O resources (e.g., tapes, disks, I/O channel s) in response to requests from user processes. The derivation employs the UNITY methodology [2], which nicely captures the concurrent inter action of the I/O subsystem with its environment. The verified resourc e 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 methodo logy, the derivation illustrates a number of techniques for organizing large specifications and proofs.