VERIFY is a tool for checking finite state real-time systems in
the temporal logic RTTL. Each process in the system to be verified
is declared, in Prolog, as a transition system with lower and upper
time bounds on each transition (0 and ∞ if the bounds are
unknown). The processes can be composed in parallel to form more
complex systems of concurrent processes. To check an RTTL
property (such as freedom from deadlock or a real time response
property), VERIFY generates a state reachability graph, and
checks the RTTL property over the reachability graph. The
processes may have data variables so that various data types and
operations on data can be accommodated. If the property does not
hold, the state (or sequence of states) for which the property fails
to hold is provided. This information is useful in debugging the
design.
VERIFY is part of a toolset that is being developed at York
University (Canada) for the design of real-time safety critical
systems. The TTM/RTTL framework forms the underlying
theoretical basis for the tools. TTMs are timed transition
systems, and RTTL stands for real-time temporal logic.
Another tool called BUILD is currently under development. BUILD is a
visual specification tool for constructing complex systems as
hierarchical TTMs. BUILD also allows for the execution of the TTMs,
as well as producing the input Prolog descriptions of the systems
as Prolog code suitable for input to VERIFY.