To get an overview over the structure of the specifications of the first layer you can have a look at the development graph. We describe the important specifications bottom-up

- The project starts with the definition of an (arbitrary) supplementary predicate 'fair' and defines behaviors .
- Based on the behavior of a concrete and abstract system, refinement of fair transition systems and generalized fair forward simulations are defined.
- Correctness is proved: existence of a generalized fair forward simulation implies fair refinement.
- For completeness, the (bi-deterministic) specification Det(M,Sup) is defined, which has as states pairs of behaviors of M and a counter value, that is incremented in transitions (as long as the counter is less than the length of the behavior). It is proved that this specification has essentially the same behaviors as the original specification.
- Finally completeness is proved: a generalized fair forward simulation exists between Det(M,Sup) and (AM,ASup) provided that the refinement of (M,Sup) to (AM,ASup) is correct. The proof is by first adding an axiom for the choice functions c2a, c2i, c2j to the definition of fair refinement (between (CM,CSup) and (AM,ASup)). Then the machine (CM,CSup) is instantiated with (M,Sup) and the definition of BiDet(M,Sup) is added. Finally (CM,CSup) in the definition of generalized fair forward simulation is instantiated with the resulting specification. This gives the axioms of of generalized fair forward simulation as proof obligations for a fair refinement from (AM, ASup) to (Bidet(M,Sup)).

The structure of the specifications of the second layer is also visualized by a development graph. The proof is not done by instantiating the one of transitions systems, but separately. Therefore the structure of the specifications is nearly identical to the first layer, although the formulas and proofs needed are somewhat more complex, due to the presence of failing (diverging) ASM rules.

- The project starts with the definition of an (arbitrary) supplementary predicate 'fair' and defines ASM behaviors .
- Based on the behavior of a concrete and abstract ASM, refinement of fair ASMs and generalized fair forward simulations are defined.
- Correctness is proved: existence of a generalized fair forward simulation implies fair refinement.
- For completeness, the (bi-deterministic) specification Det(M,Sup) is defined, which has as states pairs of behaviors of M and a counter value, that is incremented in transitions (as long as the counter is less than the length of the behavior). It is proved that this specification has essentially the same behaviors as the original specification.
- Finally completeness is proved: a generalized fair forward simulation exists between Det(M,Sup) and (AM,ASup) provided that the refinement of (M,Sup) to (AM,ASup) is correct. The proof is by first adding an axiom for the choice functions c2a, c2i, c2j to the definition of fair refinement (between (CM,CSup) and (AM,ASup)). Then the machine (CM,CSup) is instantiated with (M,Sup) and the definition of BiDet(M,Sup) is added. Finally (CM,CSup) in the definition of generalized fair forward simulation is instantiated with the resulting specification. This gives the axioms of of generalized fair forward simulation as proof obligations for a fair refinement from (AM, ASup) to (Bidet(M,Sup)).

- The basic KIV library with basic data types

Here you can find all our publications.

Back to the overview of all KIV projects .

For general informations on KIV and a download site for the whole system refer to this page.

[Impressum] [E-Mail]