The University of Waikato - Te Whare Wānanga o Waikato
Centre for Open Software Innovation Research Centre
Home Waikato Home  >  COSI  >  Projects  >  Formal Methods  >  WATERS Staff + Students Login |  - Logout

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.

Formal Methods Group

Project homepage

GPL 2

ChooseWaikato

Apply Now!