REACTO Verification System Project

The REACTO system supports formal verification of reactive systems specified as hierarchical finite state machines. Reacto has been used to specify DES code machines, interactive electronic technical manuals for aircraft maintenance, and other reactive systems. It provides:

REACTO may be used in both batch and interactive mode to develop and/or verify a high-level specification. The specification can then be transformed into a target implementation language such as C, Ada, or Lisp.