Title :
An exercise in verifying concurrent programs in industry: the I/O subsystem
Author :
Staskauskas, Mark G.
Author_Institution :
Dept. of Comput. Sci., Texas Univ., Austin, TX, USA
Abstract :
The author describes the formal verification of a portion of an existing mainframe operating system using the UNITY methodology proposed by K.M. Chandy and J. Misra (1988). The UNITY methodology consists of a programming notation and a logic for specifying and reasoning about properties of parallel programs. The author discusses the steps involved in specifying the operating system, deriving from the specification a correct UNITY program, and using the latter to drive the assembly language implementation of the system. He also comments on his experience in applying a formal methodology in the context of a large software project
Keywords :
formal specification; parallel programming; program verification; I/O subsystem; UNITY methodology; assembly language implementation; concurrent programs verification; formal methodology; formal verification; large software project; parallel programs; programming notation; Application software; Assembly systems; Computer industry; Drives; Formal verification; Logic programming; Operating systems; Resource management; Software design; Software quality;
Conference_Titel :
Computers and Communications, 1991. Conference Proceedings., Tenth Annual International Phoenix Conference on
Conference_Location :
Scottsdale, AZ
Print_ISBN :
0-8186-2133-8
DOI :
10.1109/PCCC.1991.113829
