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

fYear

1991

fDate

27-30 Mar 1991

Firstpage

325

Lastpage

331

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computers and Communications, 1991. Conference Proceedings., Tenth Annual International Phoenix Conference on

Conference_Location

Scottsdale, AZ

Print_ISBN

0-8186-2133-8

Type

conf

DOI

10.1109/PCCC.1991.113829

Filename

113829