Verifier

The verifier is to check safety and liveness properties by on-the-fly exploration of the state-space of a system in terms of symbolic states represented by constraints. The verification tool in UPPAAL also provides a requirement specification editor for specifying and documenting the system requirements.

In this help section we describe how to operate the verification tool, in terms of how to specify and verify requirements. The requirement specification language and the verification options are described in separate sections.