Mutual Exclusion in a Token Ring in CC++

Binau, Ulla (1992) Mutual Exclusion in a Token Ring in CC++. Technical Report. California Institute of Technology. [CaltechCSTR:1992.cs-tr-92-11]

Full text available as:

	Postscript - Requires a viewer, such as GhostView
	Other (Adobe PDF (260KB))

Abstract

This report describes a first attempt at using UNITY to verify reactive Compositional C++ (CC++) programs. We propose a distributed solution to the mutual exclusion problem using partially synchronous communication channels. The solution is described as a CC++ program, from which a small set of "basic" properties is derived. Using UNITY, we proof mutual exclusion and progress of the solution based on the set of properties derived from the code.

EPrint Type:	Monograph (Technical Report)
Subjects:	All Records
ID Code:	104
Deposited By:	Caltech Library System
Deposited On:	25 April 2001
Record Number:	CaltechCSTR:1992.cs-tr-92-11
Official Persistent URL:	http://resolver.caltech.edu/CaltechCSTR:1992.cs-tr-92-11
Usage Policy:	You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.

Archive Staff Only: edit this record