The Tempo Language User Guide and Reference Manual Nancy A. Lynch, Stephen J. Garland, Dilsun Kaynar, Laurent Michel, Alex Shvartsman Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology February 3, 2008Abstract Tempo is a simple formal language for modeling distributed systems with (or without) timing constraints, as collections of interacting state machines called Timed Input/Output Automata. Tempo provides natural mathematical notations for describing systems, their properties, and rela-tionships between their descriptions at different levels of abstraction. An associated Tempo Toolkit supports several validation methods for systems described using Tempo, including static analysis, simulation, interactive proof using the PVS theorem-prover, and model-checking using the Uppaal model-checker. This three-part document consists of: (I) an informal tutorial that describes the underlying mathematical Timed Input/Output Automata framework and demonstrates how to use the Tempo language to model typical timed systems; (II) a systematic description of the Tempo language constructs; and (III) a reference manual containing a complete definition of the Tempo language.iiContents 1 Introduction 1 1.1 Timed I/O Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Intended applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.3 The Tempo language and tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 I Tempo Language Tutorial 4 2 Tutorial Introduction 4 3 The Timed I/O Automata Mathematical Framework 4 3.1 Timed I/O Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.2 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.3 Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.4 Operations on Timed I/O Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 4 Example 1: Fischer’s Timed Mutual Exclusion Algorithm 8 4.1 Overview of the algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.2 Tempo description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.3 Properties of the algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 5 Example 2: Two-Task Race System 16 5.1 The algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 5.2 The behavior specification and simulation relation . . . . . . . . . . . . . . . . . . . 19 5.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 6 Example 3: Timeout-Based Failure Detector 23 6.1 The timed channel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.2 The sender . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6.3 The receiver process . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 6.4 The complete timeout system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 6.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 7 Example 4: Leader-Election Algorithm 29 7.1 The election processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 7.2 The failure-detection service . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 7.3 The complete leader-election system . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 7.4 Discussion . . . . . . . . . . . . . . . . . . . . . . …
View Full Document