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.