Architecture
Attestor is organized in phases which are executed sequentially, 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.
Depending on the atomic propositions which occur in supplied LTL specifications, we first perform grammar refinement. After that, the abstraction preprocessing phase computes the actual transformers used in the state space generation algorithm, i.e. canonicalisation, materialisation, garbage collection, assignment of atomic propositions, etc.
The figure below illustrates a high-level perspective of the state space generation loop (without procedure calls). The state space generation loop attempts to discover new program states until a fixed point is reached. To this end, the abstract program semantics is applied, i.e. states are concretised such that the concrete semantics can be executed. After that, during rectification, program states are cleaned up. For example, the garbage collector is executed. The resulting states are then abstracted, labeled with atomic propositions, and inserted into the state space if they are not subsumed by already existing states.
The model checking phase attempts to verify every supplied LTL specification for the previously generated state space. For each specification, there are three possible outcomes:
- The specification is satisfied.
- The specification is violated.
- The state space generation was prematurely aborted, e.g. by exceeding a threshold. In this case, it is unknown whether a specification holds.
If a previously checked LTL specification is violated, a (potentially spurious) counterexample is generated. Furthermore, it is possibly to verify that a counterexample is not spurious and obtain a concrete input triggering a violation of the specification in question.
The output of Attestor consists of
- the abstract state space obtained during state space generation,
- contracts generated for all methods encountered during state space generation,
- the model checking results for all supplied LTL specification, i.e. satisfied, violated and a counterexample, or unknown.
The Attestor API gives access to the state space, generated contracts results, counterexamples, execution times for all phases, and the sizes of generated state spaces.
The Attestor frontend allows graphical exploration of state spaces, counterexamples, contracts, and supplied grammars.