Refinement of Parallel and Reactive Programs

Back, R.J.R. (1992) Refinement of Parallel and Reactive Programs. Technical Report. California Institute of Technology. [CaltechCSTR:1992.cs-tr-92-23]

Full text available as:

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

Abstract

We show how to apply the refinement calculus to stepwise refinement of parallel and reactive programs. We use action systems as our basic program model. Action systems are sequential programs which can be implemented in a parallel fashion. Hence refinement calculus methods, originally developed for sequential programs, carry over to the derivation of parallel programs. Refinement of reactive programs is handled by data refinement techniques originally developed for the sequential refinement calculus. We exemplify the approach by a derivation of a mutual exclusion algorithm.

EPrint Type:	Monograph (Technical Report)
Subjects:	All Records
ID Code:	113
Deposited By:	Caltech Library System
Deposited On:	25 April 2001
Record Number:	CaltechCSTR:1992.cs-tr-92-23
Official Persistent URL:	http://resolver.caltech.edu/CaltechCSTR:1992.cs-tr-92-23
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