An exercise in verifying concurrent programs in industry: the I/O subsystem

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...

Full description

Saved in:
Bibliographic Details
Main Author: Staskauskas, M.G.
Format: Conference Proceeding
Language:English
Subjects:
Application software
Assembly systems
Computer industry
Drives
Formal verification
Logic programming
Operating systems
Resource management
Software design
Software quality
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.< >
DOI:10.1109/PCCC.1991.113829