Architecture
Attestor is organized in phases which are executed one after the other; each phase taking as an input the output of previous phases. The following picture illustrates the main components of Attestor in which several phases are grouped into one.
Apart from a Java program, a user has to provide a graph grammar to guide the generation of an abstract state space. Furthermore, it is possible to supply a specification in linear temporal logic which is verified after state space generation. In addition to that, one may supply contracts for program methods or library functions that should not be analyzed. Please confer the page on command line options for detailed explanations of the individual options to configure an analysis.
All of these inputs are parsed in their own phase.
Hence, phase Parsing Inputs actually consists of the following phases:
- Command line interface
- Parse Java jrogram
- Parse grammar
- Parse initial states
- Parse contracts