Skip to main content.

Verifying Requirements

The queries (i.e. the system requirements) are verified from the verifier interface of UPPAAL. A verification is always performed according to the settings specified in the Options menu of the main menu bar.

The selected queries are verified when the button named Check is pressed. The verification output is displayed in the Status field at the bottom of the verifier panel. The result is also indicated by the circular markers in the rightmost column of the Overview panel. A grey marker indicates that the truth value of the property is unknown, a green marker that the property is satisfied, and a red marker that the property is not satisfied.

In case the Over Approximation or the Under Approximation options are enabled, the output of the verifier might be that property is "maybe satisfied". This happens when the verifier cannot determine the truth value of the property due to the approximations used.