MIT 6 852 - The Tempo Language User Guide and Reference Manual

Unformatted text preview:

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

MIT 6 852 - The Tempo Language User Guide and Reference Manual

Download The Tempo Language User Guide and Reference Manual
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view The Tempo Language User Guide and Reference Manual and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view The Tempo Language User Guide and Reference Manual 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?