🚀 go-pugleaf

The following SRC Research Report is now available:


Authors: Martin Abadi and Leslie Lamport 
Title: An Old-Fashioned Recipe for Real Time
Date: October 12, 1992
Report #91, October 12, 1992
Length: 67 pages
Availability: anonymous FTP from gatekeeeper.pa.dec.com
Directory: /pub/DEC/SRC/research-reports/




Authors' abstract:

Traditional methods for specifying and reasoning about concurrent
systems work for real-time systems. Using TLA (the temporal logic of
actions), we illustrate how they work with the examples of a queue and
of a mutual-exclusion protocol. In general, two problems must be
addressed: avoiding the real-time programming version of Zeno's
paradox, and coping with circularities when composing real-time
assumption/guarantee specifications. Their solutions rest on properties
of machine closure and realizability.


===========================================================================
Co-moderator:  Richard Golding, Computer & Information Sciences, UC Santa Cruz
	    compdoc-techreports-request@ftp.cse.ucsc.edu