Σοφία User Manual
Before following any instructions in this document, make sure you have performed
the setup tasks described in the Installation
Instructions. This manual will walk you through the use of the various tools
provided by Σοφία. Please note that at this time, all of the
tools in Σοφία are command-line driven.
The instructions in this manual are for version 2.0.0 of Σοφία,
and may not be applicable to earlier versions. To check what version of
Σοφία you are using, run the command:
java sofya.base.ProjectDescription
You should see the version number printed on your console.
This manual is organized into the following sections. In many cases, these
sections correspond to the Java packages found in Σοφία.
- General: This section describes general features of Σοφία and
activities that may need to be performed before using the tools in
Σοφία.
- Graph Tools: This package provides the implementations and tools to construct various
kinds of graphs, most notably control flow graphs (CFGs). The graphs
constructed here are used by various other tools throughout the system.
- Event dispatch framework: This package contains the framework for dispatching event streams of specified
program observations. The instrumentors, event dispatchers, and event
selection filters for semantic and structural event streams are found in this
package. This is also the place to find information about collecting various
types of trace files provided by Σοφία.
- Tools: This package provides tools to perform various analyses using the outputs
generated by other components.
- Java mutation fault toolkit: This package provides a Java bytecode mutator used for creating mutation faults
based on a variety of mutation operators. It is built on a dynamic framework
that is easily extended to implement new mutation operators.
- File Viewers: These are used to view the outputs generated by other components of
Σοφία, such as control flow graphs, trace files,
and test histories.
- Applications: This package contains example applications built using the Σοφία
framework. These applications are functional and may be useful for actual software
verification.
If you are inclined to building Σοφία we offer some
guidance in the
building Σοφία page.
Author: Alex Kinneer © 2006 University of Nebraska - Lincoln.