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 descrip tions (the Build tool), Visual state descriptions allow the designer t o browse and understand the structure of the system, A timing hierarch y of spontaneous, just, and forced timed events, and a variety of comp utational notions such as concurrency, hierarchy, nondeterminism, proc ess interaction, and communication can be represented. The combination of model-checking (the Verify tool) and theorem proving allows for th e treatment of finite and infinite state systems, The toolset is illus trated with a shutdown controller of a reactor, as taken from an actua l industrial requirements document in which the system is described in formally using a mixture of English descriptions, timing diagrams, and pseudocode. Using StateTime, a unified precise description of the shu tdown reactor is obtained, which can then be checked automatically for conformance with its requirements.