A visual toolset for the design of real-time discrete-event systems

StateTime is a prototype toolset that supports the design of verified real-time discrete-event systems using executable visual state descriptions (the Build tool). Visual state descriptions allow the designer to browse and understand the structure of the system. A timing hierarchy of spontaneous, just, and forced timed events, and a variety of computational notions such as concurrency, hierarchy, nondeterminism, process interaction, and communication can be represented. The combination of model-checking (the Verify tool) and theorem proving allows for the treatment of finite and infinite state systems. The toolset is illustrated with a shutdown controller of a reactor, as taken from an actual industrial requirements document in which the system is described informally using a mixture of English descriptions, timing diagrams, and pseudocode. Using StateTime, a unified precise description of the shutdown reactor is obtained, which can then be checked automatically for conformance with its requirements