SRC Research Report 15

A Simple Approach to Specifying Concurrent Systems.

Leslie Lamport.

In the transition axiom method, safety properties of a concurrent system can be specified by programs; liveness properties are specified by assertions in a simple temporal logic. The method is described with some simple examples, and its logical foundation is informally explored through a careful examination of what it means to implement a specification. Language issues and other practical details are largely ignored.

Back to the SRC Research Reports main page.

• PostScript compressed with UNIX compress -- 112 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 88 Kbytes
  
• PostScript compressed with ZIP -- 88 Kbytes
  
• PostScript -- 288 Kbytes
  
• Portable Document Format (PDF) -- 304 Kbytes