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 Check is pressed.
The verification progress dialog displays the following statistics:
- Property number out of total number of properties asked to be verified.
- Load
- the number of states in the waiting list. The verification is over when the waiting list becomes empty. The waiting list grows when new state successors are added. SMC algorithms do not use waiting list.
- CPU time usage
- Processor time usage: the actual verification time is in blue, and operating system (OS) time is in red. OS time may indicate swapping and thrashing, lack of verification time indicates lack of computation (and thus verification progress).
- RAM usage
- Random access memory usage: actual verification storage is in blue, other (unrelated) processes are in gray and operating system cache and buffers are in yellow, the rest is free. Cache and buffers may also be considered as free. OS may swap some memory out onto disk, especially if there is lack of free memory. Verification may become inefficient if its memory is being swapped out and computer may become unresponsive if verifier takes over almost all memory.
- Swap usage
- Swap disk usage: actual verification storage is in blue, other (unrelated) are in grey. Operating system may crash if no memory and no swap space is left.
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.
Status also reports the resources used by verifier:
- Time used
- Verification time is the processor time spent on verification, kernel time is the operating system time spent on servicing (loading, swapping, input-output etc), elapsed time is the wall-clock time from verification start to finish.
- Memory usage peaks
- Peak is the maximum memory used throughout the verification process. Virtual memory is the amount of memory requested by the verification process. Resident memory (also called working set) is the actual amount of RAM allocated by an operating system which is smaller than virtual memory as the rest of virtual memory may be swapped out or not used at all.
In addition, the command line utility verifyta may provide more statistics. For example:
- States stored
- The number of states kept in memory. State storage is necessary to ensure the termination of the state space exploration. Not all states are stored: committed states are not stored, also progress measure (sweep-line method) may allow reuse of memory.
- States explored
- The number of states that have been checked and successors computed.
Notice that the tool does not report the total number of states: symbolic queries deal with symbolic states (using zones), which encode infinite number of concrete states (such statistic is meaningless), the size and shape of each symbolic state depends on the exploration order, moreover not all states are stored, some may be explored multiple times without any indication, therefore such accounting is subjective to the algorithm used and does not indicate the complexity of a given model. Whereas the tool performance is better reflected by the processor time and memory usage.
Note that the resource figures do not include an overhead of UPPAAL GUI, and the measurements are done in ~1s snapshots, this monitoring effort is included into verification time and in principle some memory usage peaks may be missed.
Alternatively memtime can be used on verifyta: it does not depend on repeated snapshots, does not impose monitoring overhead, is more precise and therefore is a preferred method.
Some figures are not available on some OSes (e.g. system cache allocation is not documented in Windows API, swap usage per process is not maintained by Linux kernel), and thus cannot be displayed.
Statistical Model Checking
Parameters for statistical model checking can be changed in the Options menu. Various data plots (if available) can be accessed via popup-menu by right-clicking the statistical property. The y-axis always denotes a probability or its density, while x-axis denotes either the variable values limited by the statistical query or a step (transition) count in the model run.
- Probability density distribution
- A histogram created from probability distribution where each bucket is normalized by a bucket width.
Useful for comparison of various distributions, potentially with different bucket widths.
- Probability distribution
- A histogram created from a frequency histogram where each bucket is normalized by a total number of runs.
Useful for assessing a probability of a property being satisfied at a particular moment in time interval.
- Cumulative probability distribution
- A histogram created by adding up all frequency histogram buckets up to the current bucket and normalized by a total number of runs.
- Confidence Intervals for Probabilities
- The confidence intervals for probabilities are computed using Clopper-Pearson method (also known as "exact") for binomial distribution for a given level of confidence (1-α).
The method is conservative in a sense that it guarantees the minimum coverage of the real probability in (1-α) of cases.
In the plots, the estimated confidence is valid only for one bucket at a time (the gathered data is reused to compute each individual bucket).
- Confidence Intervals for Mean
- The confidence intervals for mean estimation are computed using quantiles of Student's t-distribution for a given level of confidence of 1-α.
Note that t-distribution approaches the commonly used Normal (Gaussian) distribution when the number of samples is high.
- Frequency histogram
- The frequency histogram is created by calculating the number of runs satisfying the property at a particular moment in time interval.
Useful for calculating the number of runs.
Plot appearance can be customized from a popup menu by right-clicking on the plot. Furthermore, the plot labels and titles can be edited, and several data sets can be superimposed in one figure by using Plot Composer, accessible from the Tools menu. It is possible to create several composite plots at a time by invoking Plot Composer multiple times.
An extensive overview and comparison of methods for computing confidence intervals for binomial distribution can be found in the following publications:
Interval Estimators for a Binomial Proportion: Comparison of Twenty Methods, Ana M. Pires and Conceicao Amado. REVSTAT -- Statistical Journal, Vol.6, No.2, June 2008, pages 165-197.
Interval Estimation for a Binomial Proportion, Lawrence D. Brown, T. Tony Cai and Anirban DasGupta. Statistical Science, 2001, Vol.16, No.2, pages 101-133.