Formal derivation of concurrent programs: an example from industry

Author

Staskauskas, Mark G.

Author_Institution

Dept. of Comput. Sci., Texas Univ., Austin, TX, USA

Volume

19

Issue

5

fYear

1993

fDate

5/1/1993 12:00:00 AM

Firstpage

503

Lastpage

528

Abstract

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

Keywords

formal specification; parallel programming; program verification; I/O channels; I/O subsystem; UNITY methodology; concurrent programs; disks; formal derivation; operating system; proofs; resource allocation algorithm; specifications; tapes; Algorithm design and analysis; Application software; Design engineering; Information systems; Logic programming; Operating systems; Organizing; Resource management; Software algorithms; Software design;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.232015

Filename

232015