The Waikato Analysis Tool for Events in Reactive Systems
This software enables users to create finite-state machine models in a graphical user interface, to simulate their execution, and to apply model checking algorithms to them. Its main features are/will be: * graphical modelling of complex finite-state machine models, using the framework of discrete-event systems; * animation of several finite-state machines running in parallel; * push-button verification of finite-state machine models, i.e., checking whether a model satisfies certain properties and displaying diagnostic information if it does not. Waters is intended to support research and teaching in the area of model checking and discrete-event systems. It includes features to create large-scale and parameterised extended finite-state machine models, and to experiment with different model checking algorithms. The tool may also be used by software developers who write safety-critical code and want to check whether it is correct. WATERS is part of Supremica.