RoboTool supports graphical modelling, validation, and automatic generation of mathematical definitions for proof of properties of RoboChart models, with proof automated using model checking. The RoboChart notation is distinctive in its features that support architectural modelling as well as timed constructs in state machines.
This repository provides a complete RoboTool install, both as a setup file for installation using the Eclipse installer, as well as self-contained releases that can be executed directly after downloading. The latter contain a Java JRE for the target platform.
The RoboTool manual describes in detail how to use the tool. Documentation for notations is available from the RoboStar notations page.