Back to Search Start Over

A mechanized process algebra for verification of device synchronization protocols

Authors :
Schubert, E. Thomas
Source :
Idaho Univ., The 1992 4th NASA SERC Symposium on VLSI Design.
Publication Year :
1992
Publisher :
United States: NASA Center for Aerospace Information (CASI), 1992.

Abstract

We describe the formalization of a process algebra based on CCS within the Higher Order Logic (HOL) theorem-proving system. The representation of four types of device interactions and a correctness proof of the communication between a microprocessor and MMU is presented.

Subjects

Subjects :
Computer Programming And Software

Details

Language :
English
Database :
NASA Technical Reports
Journal :
Idaho Univ., The 1992 4th NASA SERC Symposium on VLSI Design
Notes :
NAS1-18586
Publication Type :
Report
Accession number :
edsnas.19940017243
Document Type :
Report