Today’s technical systems become more and more software-intensive which typically means that software is the major component that provides the needed functionality. For example, nowadays 50% of the total costs of the development of an airplane go into software development. Moreover, only 6% of these expenses are spent on the actual development of the software system, and about 44% are consumed by testing, verification and validation activities. Consequently, considerations concerning reliability and dependability become more and more important, and formal methods offer themselves back to the software engineering community.

The use of formal specifications seem to be a silver bullet, but there are a couple of drawbacks:

• Not all stakeholders are familiar with the formal notation(s).
• The mathematically dense notation(s), combined with the inherent complexity of the system, impedes the understanding of the specified system.
• Without tool support, it takes a lot of effort to keep specifications up-to-date (and at high quality) during the development live-cycle.

The ViZ project focuses on these impediments and, for the Z specification language, looks for solutions to the above mentioned impediments:

• It addresses the fact of software evolution in respect to formal specifications and defines a measurement system for focusing on complexity and quality attributes.
• It deals with the issue of the transformation of formal specifications. In order to support different stakeholders in a project, formal specifications are enriched by UML notations.
• It deals with the maintenance support for large and complex formal specifications. It presents a concept location model, the necessary tool-sets for the related comprehension tasks and also a system for storing and retrieving concepts into and from a database.

The ViZ environment consists of several sub-projects which are currently being integrated into a single Eclipse plugin:

• A metrics plugin which is currently being integrated into the Eclipse environment. It is available as a standalone version at the moment and further developed in the master thesis of F. Radl.
• A concept-location plugin (for ASRN graph, PrimeTree, Slicing and Chunking generation/visualization) making use of the graphviz environment.
• A transformation plugin that maps Z specifications to UML class and activity diagrams. The implementation is based on the master thesis of J. Lessacher.
• (Experimental!) A storage pluguin that maps the specification to a database and supports retrieving specification abstractions. The plugin is based on the master thesis of D. Pohl.