Summary of Changes since Version 1
Warning
This page is under construction.
Why Version 2?
Version 2 of the UV system is the result of a significant
restructuring of the UV system architecture. There were mainly three
reasons for doing such a redesign:
- In order to make the system more easily available and to avoid
licensing problems, we wanted to get away from OSF Motif.
- As a platform for our own research a much more flexible and
modifiable user interface structure was needed.
- The UV system had slowly evolved over two years, some of its
initial design decisions had become obsolete whereas other desired
features could not be added easily. This required a substantial
cleanup of the code.
As a result of the restructuring process version 2 of the UV system
differs from the original system significantly with respect
to its user interface, its system structure, and the expressiveness of
the input language used for stating programs and properties.
Although not all features of version 1 have been moved to version 2
yet, and although not all envisioned extensions are completed yet, the
main differences of version 2 over version 1 can be summarized under
the following three feature sets.
User Interface based on Tcl/Tk
Version 2 uses Tcl/Tk for its user interface. The UNITY Verifier
Shell uvwish provides the basic system functionality for
parsing UNITY programs and properties and for invoking the model checker,
whereas the entire user interface is written as Tcl/Tk scripts that are
interpreted by uvwish.
Workspace Architecture for Scriptable System Operations
During a verification session all important entities like programs,
properties, or invariants are not only maintained by the UV system,
but are also available through the Tcl scripting interface.
Extensions to the UV Input Language
Syntactic constructs for defining transparent variables (in the
always-section) and for synchronous composition of statements have been
provided. The type system has been cleaned up and has been extended by
record types and mappings (a generalization of finite state arrays).
Other extensions such as quantified statements and program composition
are planned.
This page was last updated on 25-May-1996.
markus@cs.utexas.edu