home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #1 / NN_1993_1.iso / spool / comp / doc / techrepo / 230 < prev    next >
Encoding:
Internet Message Format  |  1993-01-05  |  1.4 KB
  1. Path: sparky!uunet!usc!cs.utexas.edu!sun-barr!olivea!hal.com!darkstar.UCSC.EDU!golding
  2. From: src-report@src.dec.com (James Mason)
  3. Newsgroups: comp.doc.techreports
  4. Subject: SRC Research Report #91
  5. Message-ID: <1ic5hmINNkb3@darkstar.UCSC.EDU>
  6. Date: 5 Jan 93 14:21:42 GMT
  7. Organization: DEC Systems Research Center
  8. Lines: 29
  9. Approved: compdoc-techreports@ftp.cse.ucsc.edu
  10. NNTP-Posting-Host: oak.ucsc.edu
  11. Originator: golding@oak
  12.  
  13. The following SRC Research Report is now available:
  14.  
  15.  
  16. Authors: Martin Abadi and Leslie Lamport 
  17. Title: An Old-Fashioned Recipe for Real Time
  18. Date: October 12, 1992
  19. Report #91, October 12, 1992
  20. Length: 67 pages
  21. Availability: anonymous FTP from gatekeeeper.pa.dec.com
  22. Directory: /pub/DEC/SRC/research-reports/
  23.  
  24.  
  25.  
  26.  
  27. Authors' abstract:
  28.  
  29. Traditional methods for specifying and reasoning about concurrent
  30. systems work for real-time systems. Using TLA (the temporal logic of
  31. actions), we illustrate how they work with the examples of a queue and
  32. of a mutual-exclusion protocol. In general, two problems must be
  33. addressed: avoiding the real-time programming version of Zeno's
  34. paradox, and coping with circularities when composing real-time
  35. assumption/guarantee specifications. Their solutions rest on properties
  36. of machine closure and realizability.
  37.  
  38.  
  39. ===========================================================================
  40. Co-moderator:  Richard Golding, Computer & Information Sciences, UC Santa Cruz
  41.         compdoc-techreports-request@ftp.cse.ucsc.edu
  42.