RTDT: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams

Nina Amla, E. Allen Emerson, Robert P. Kurshan and Kedar Namjoshi

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001

Abstract

In this paper, we outline the key features of the tool Rtdt, which is based on a visual specification formalism called Synchronous Regular Timing Diagrams (SRTD's). Rtdt consists of an editor that allows a user to graphically create and edit an SRTD. The tool implements an efficient model checking algorithm that is linear in both the size of the system and the SRTD specification. Rtdt also implements a sound and complete assume-guarantee proof rule that can be applied to SRTD's in a fully automated way.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems