Clements, P.C., C.L. Heitmeyer, B.G., Labaw and A.T., Rose, "MT: A
Toolset for Specifying and Analyzing Real-Time Systems",
Proceedings of the Real-Time Systems Symposium, IEEE Computer Society, 
Raleigh-Durham, North Carolina, 1994. 

<blockquote>
This paper introduces MT, a collection of integrated tools for
specifying and analyzing real-time systems using the Modechart
language.  The toolset includes facilities for creating and editing
Modechart specifications.  Users may symbolically execute the
specifications with an automatic simulation tool to make sure that the
specified behavior is what was intended.  They may also invoke a
verifier that uses model-checking to determine whether the
specification imply (satisfy) any of a broad class of safety
assertions.  To illustrate the toolset's capabilities as well as
several issues that arise when formal methods are applied to
real-world systems, the paper includes specifications and analysis
procedures for a software component taken from an actual Navy
real-time system.
</blockquote>