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:

• Local variables scoped with respect to the state hierarchy
• A functional sub-language for specifying state-transition predicates and actions
• An abstract interface for specifying communication with the external environment
• A powerful theorem prover for verifying user-defined assertions
• Graphical support for specification acquisition and simulation

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.