In the present form AGREE consistency checks are weak and realizability checks are fragile. Current work at the U of Minnesota CriSys has developed a stronger and more robust check: AE-VAL. The scope of this issue is to discuss the integration of the AE-VAL mechanism with AGREE as the default consistency/realizability checking mechanism.
Further, consistency analysis is done at all layers with is potentially extra work. The analysis need only be done at the top layer and at each of the leaf type contracts. @mwwhalen describes the rationale behind this as follows:
At the leaf level, there are no AGREE proofs; we rely on the contracts to be well-formed for the compositional proof procedure. What we would really like here is to have implementations that are proved correct with respect to the leaf-level contracts: this demonstrates that the contracts are realizable. In the absence of such implementations and proofs, we developed the realizability check in order to determine whether an implementation can be constructed. The version that is in the current AGREE tool is still (I think) based on k-induction and doesn't scale too well and may claim a contract is unrealizable when in fact it can be realized. Andreas has a more recent implementation based on PDR that scales better and is sound for both realizable and unrealizable results.
When "wiring together" a subsystem, each subcomponent assigns a disjoint subset of the variables of the composition. For each subcomponent contract, realizability states that for any infinite input trace satisfying the assumptions, there is a possible output output trace. With the "wiring" the outputs of one subcontract will either a.) violate the assumptions of another contract (this is checked via proof) or b.) be a trace within the realizable set (by assumption of component realizability). So, either the proof fails, or the wired system is realizable.
Given a proof, since the contract at this next level is implied by the leaf-level contracts, it allows the same or strictly more behaviors than the "wired together" subsystem with their contracts. Thus, if the "wired together" system is realizable, the contract at the next level is realizable.
The same thing is true if we replace "realizable" with "consistent".
This is why we don't need to check consistency or realizability at any level other than the leaf level during "verify all layers". When you are working on a particular layer (even not at the leaf), these checks are still useful! You may be having difficulty proving the system level properties, and if you know that the composition is inconsistent or the contract is unrealizable, you know that you have to fix the system-level properties.
One thing that should also be changed: the current default for consistency checking is still depth 1. This is almost useless. The depth should be at least, say, 5, so that the system can show some behavior.
Accordingly the best-practice development process for the models is to, as the layers are being developed perform a single-layer verification. In this case the leaves are the immediate type contracts and the top is the component implementation being analyzed. Accordingly, there are no intermediate nodes.
Once the model is fully developed and all failed obligations have been fixed, then an analysis across all layers is run to produce the final evidence of the completed model. This analysis checks consistency at the top layer verify that the assumptions are consistent, assume-guarantee contract analysis for each implementation in the model hierarchy, and consistency checks at the leaf nodes to verify they are consistent and realizable.
Thus, it is deemed to not be necessary to retain an option to analyze intermediate compositions or type contracts for consistency/realizability. The AGREE User's guide should be updated to describe correct application of this process.
In the present form AGREE consistency checks are weak and realizability checks are fragile. Current work at the U of Minnesota CriSys has developed a stronger and more robust check: AE-VAL. The scope of this issue is to discuss the integration of the AE-VAL mechanism with AGREE as the default consistency/realizability checking mechanism.
Further, consistency analysis is done at all layers with is potentially extra work. The analysis need only be done at the top layer and at each of the leaf type contracts. @mwwhalen describes the rationale behind this as follows:
Accordingly the best-practice development process for the models is to, as the layers are being developed perform a single-layer verification. In this case the leaves are the immediate type contracts and the top is the component implementation being analyzed. Accordingly, there are no intermediate nodes.
Once the model is fully developed and all failed obligations have been fixed, then an analysis across all layers is run to produce the final evidence of the completed model. This analysis checks consistency at the top layer verify that the assumptions are consistent, assume-guarantee contract analysis for each implementation in the model hierarchy, and consistency checks at the leaf nodes to verify they are consistent and realizable.
Thus, it is deemed to not be necessary to retain an option to analyze intermediate compositions or type contracts for consistency/realizability. The AGREE User's guide should be updated to describe correct application of this process.