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 program
- Parse grammar
- Parse initial states
- Parse contracts
Some LTL specifications require that nodes in a program state are tracked along sequences of states.
For example, to prove that every node is eventually visited by a variable x, we fix an arbitrary node in an initial state and track it along all sequences leading to termination. Whenever variable x equals that tracked node in a state, a corresponding atomic proposition {visited(x)} is assigned to that state.
Notice that we have to fix an arbitrary node in the above example. In other words, we have to consider all variants of the initial states in which different nodes have been fixed. Nodes are fixed by a marking, i.e. a special variable that is never accessed by the program and that is attached to the node that should be fixed. The marking generation phase is responsible for computing the set of all initial states with different markings. Actual markings are determined by the atomic propositions occurring in supplied LTL specifications.
