Open Systems in TLA

We describe a method for writing assumption/guarantee specifications of concurrent systems. We also provide a proof rule for reasoning about the composition of these systems. Specifications are written in TLA (the Temporal Logic of Actions), and all reasoning is performed within the logic. Our proof rule handles internal variables and both safety and liveness properties.

• Type: Conference
• Year: 1994
• Where: PODC
• Authors: Martín Abadi, Leslie Lamport
• Keywords: Assumption/guarantee Specifications, Concurrent Systems, Distributed And Parallel Computing, PODC 1994, Proof Rule