CaltechAUTHORS
  A Caltech Library Service

Mutual Exclusion in a Token Ring in CC++

Binau, Ulla (1992) Mutual Exclusion in a Token Ring in CC++. California Institute of Technology . (Unpublished) http://resolver.caltech.edu/CaltechCSTR:1992.cs-tr-92-11

[img]
Preview
Postscript
See Usage Policy.

202Kb
[img]
Preview
Other (Adobe PDF (260KB))
See Usage Policy.

253Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:1992.cs-tr-92-11

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.


Item Type:Report or Paper (Technical Report)
Group:Computer Science Technical Reports
Record Number:CaltechCSTR:1992.cs-tr-92-11
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.
ID Code:26755
Collection:CaltechCSTR
Deposited By: Imported from CaltechCSTR
Deposited On:25 Apr 2001
Last Modified:26 Dec 2012 14:04

Repository Staff Only: item control page