An Brief Introduction to the UV System
An Brief Introduction to the UV SystemUNITY is given a state-based transition system semantics and derives much of its simplicity from abstracting away from the notion of control flow. A UNITY program is essentially a bag of multiple assignment statements, a program execution consists of repeatedly selecting statments from the bag and executing them atomically (subject to the fairness constraint, that no statement be ignored forever).
Properties of UNITY logic can be devided into safety and progress properties. A typical safety property is the invariant property stating that some predicate invariantly holds during any program execution. For instance the property
invariant x>0states that variable x is always positive in any program execution. A typical progress property on the other hand is the leads-to property, which states that whenever some predicate holds during some state in a program execution, some (other) predicate inevitably holds at the same or a later state of that execution. For instance the property
x=0 leads-to x>0states that whenever x is equal to 0 during any program execution, it is positive at some later point in the execution.
In spite of its simplicity UNITY logic is sufficiently expressive for many interesing specifications that arise when designing concurrent programs.
There is by now a vast amount of literature available on model checking. Due to progress with symbolic representation of finite state systems and temporal logic formulae based on binary decision diagrams, model checking has become a powerful technique with applications in particular to circuit verification.
Taking advantage of the special form of UNITY temporal operators it provides a very efficient way of determining whether a given UNITY program satisfies a given formula of UNITY logic.
Programs and properties are passed as input to the system written in a ASCII based input language. Simple finite data types (boolean, finite range integer, enumeration) and all temporal operators of UNITY logic are supported.
program Mutex
declare
type PC = enum(noncritical, requesting, trying, critical, exiting);
var m, n: PC;
var u, v, p: boolean;
var hu, hv: boolean; // auxiliary variables to model non-
// deterministic behaviour of processes
// with respect to their finishing their
// critical section
always
initially
!u;
!v;
m = noncritical;
n = noncritical;
assign
// first process (u)
[u0] hu := !hu
[u1] u, m := true, requesting if hu /\ m = noncritical
[u2] p, m := v, trying if m = requesting
[u3] m := critical if !p /\ m = trying
[u4] u, m := false, exiting if m = critical
[u5] p, m := true, noncritical if m = exiting
// second process (v)
[v0] hv := !hv
[v1] v, n := true, requesting if hv /\ n = noncritical
[v2] p, n := !u, trying if n = requesting
[v3] n := critical if p /\ n = trying
[v4] v, n := false, exiting if n = critical
[v5] p, n := false, noncritical if n = exiting
end;
Two interesting properties one would like to prove for this program
are mutual exclusion and absence of starvation:
in Mutex: invariant ~(m = critical /\ n = critical); // mutual exclusion in Mutex: m = requesting --> m = critical; // absence of starvationBoth of these properties can be easily proved with the UV system either in a fully automated way (by computing the strongest invariant of the program), or by using additional invariants supplied by the user following her/his understanding of the program.
The UV system was actually used to discover some errors in the manual proofs of the above properties by showing that some of the auxiliary properties given in the original paper are not satisfied by the program.
You can also go back to the UV System(Version 2) home page, where you find more detailed information about the system and on how to use it.