Title: 	Tempo

Speaker: Laurent Michel

Place: 	32-G531
Time: 	1-2:30pm
Date: 	Friday, November 3, 2006

Abstract: 
Tempo is an integrated toolset that includes several computer-aided 
design tools for modeling, specification, and analysis of complex 
timed, concurrent, and distributed systems. The Tempo modeling 
environment and the specification language, also called Tempo, is 
based on the Timed Input/Output Automata formal framework of Kaynar, 
Lynch, Segala, and Vaandrager. The toolset includes a language 
processor (front end) that implements syntax and static semantic 
checks of the specifications expressed in Tempo, a simulator of 
system specifications, an automated tool for linking to model-checking
using UPPALL, and an automated tool for linking to theorem-proving 
using the TAME framework for PVS. The tools are integrated within a 
consistent system architecture that provides both a command-line and 
a graphical windowing interfaces for the users. The graphical interface 
is implemented with the Eclipse integrated development environment 
framework. In this talk we will overview the integration architecture,
graphical user interface, the functionality of the language processor, 
and links to the backend tools, such as the simulator, model-checking, 
and theorem-proving.
A demo of the tools accompanies the presentation.