UV Manual: Tutorial
UV Manual: Tutorial
Warning
This tutorial describes a brief sample session of the UV system. By following the tutorial you see how to
Starting up
In order to start the sample session we invoke the UV system by
executing the uv2 shell script
% uv2
If this does not work there is most likely a problem with your
set-up. Please have a look at the local access
information where you may find an explanation for your
problems.
If you run the UV system for the first time you see the following notification dialog pop up:
Read the text carefully and make your selection. You can also first look up more information about the author notification feature.
After you made your choice and the selection dialog has disappeared, you see four windows: the command window, the program table window, the property table window, and the expression table window.
In order to open the document file you select the
Open... command from the File menu
at the top of the command. A file selection dialog is displayed, with
which you can locate the
After having selected the desired file (either by pressing the
OK button or by double-clicking on the file name),
the file selection dialog disappears and is replaced by a document
window for the selected file as shown in the following figure:
In order to convert the textual description of the mutex program and
its properties into an internal form suitable for model checking, you
press the Parse command button at the top of the
document window. This causes the UV parser to process the document and
to display some progress information to the message area of the
document window. You see that parsing was successful and program
The model checker attempts to check all selected properties for the
mutex program and displays some diagnostic output in the message area
of the command window. After checking is finished you notice that the
status of all properties in the property table window has changed from
new to either ? (indicating that
the property has not been proved yet) or ok
(indicating that the property has been proved successfully):
The model checker now attempts to prove again all selected and not
yet proved properties but uses the stronger current invariant this
time. From the update status information you can observe that all
properties could be proved with the exception of properties
In particular the two most interesting properties,
It turns out, that the four properties not proved so far indeed are
not satisfied by the program. In order to confirm this with the UV
system, you have to compute the strongest invariant of the program and
use it in the model checker invocation.
You are new ready to invoke the model checker again, this time with
the strongest invariant: first select the radio button labeled with
Strongest in the option area of the property table
window, then select all the properties not proved yet (do this by
using mouse button 1 while you hold down the control key), then run
the model checker by pressing the Check Selected
Properties command button.
The model checker performs the checks and indeed reports that
the four remaining properties are not satisfied by the program by
displaying a fail status in the property table
window:
As you can see from the status information displayed in that window,
the property failed, because the safety condition (which for an
invariant property amounts to requiring that the alleged invariant
predicate is not flasified by any transition of the program) is
violated by statement
This concludes the tutorial session, you can terminate the session by
selecting the Quit command form the
File menu of the command window.
Reading a Document File
You are now ready to open a document file containing the description
of a program and of a set of properties to be checked. The program is
a simple 2-process mutual exclusion algorithms first described by Jay
Misra in Notes on Unity, 13.mutex.unity file in the
EXAMPLES subdirectory of the directory where the UV
system is installed.
#prog0 as well as properties #prop0 through
#prop12 have been entered into the workspace. As a result
of this the program and the properties are now listed in the program
table and property table windows respectively.
Invoking the Model Checker
Now that you have successfully parsed the document you can proceed to
invoke the model checker. First you do so for all properties using
only the type invariant of the program. Make sure that the checking
invariant option Type is selected with a radio button
in the option selection area of the property table window. Then simply
select all properties in the property table window (hold the first
mouse button down while moving the pointer over all property entries
in the table) and press the Check Selected Properties
buttom at the top of the property table window.
Using Invariants
Some of the successfully proved properties are invariant properties
(namely properties #prop1, #prop3,
#prop8, and #prop9) and have therefore been
automatically conjoined to the current invariant of the program. In
order to make use of this information, select the radio button
labeled with Current in the option area of the
property table window and invoke the model checker again by
pressing the Check Selected Properties command
button.#prop2, #prop4, #prop5, and
#prop6:
#prop0
which expresses the mutual exclusion of the algorithm, and
#prop12 which expresses the absence of starvation, are
successfully proved for the given program.
Using the Strongest Invariant
In order to compute the strongest invariant of the Mutex
program you simply select the entry in the program table window and
then press the Compute Strongest Invariant button at
the top of that window. The strongest invariant is computed and the
program status information is updated accordingly:
Examining a Property
Finally will have a closer look at one of the failed properties, for
instance #prop2. In order to do so, double-click on the
entry for that property in the property table window, which brings up
a property info window:
v2.
[Go back to the Manual Contents Page]
This page was last updated on 20-Nov-1995.
markus@cs.utexas.edu