Completeness of Fair ASM Refinement
This page documents the KIV specifications of the completeness proof for fair ASM refinement
as described in G. Schellhorn: Completeness of Fair ASM Refinement, submitted to FACS.
The specifications and proofs extend the ones of the
completeness proof of ASM Refinement. They add a supplementary predicate 'fair' and define
refinement based on behaviors (= fair runs).
Again, they are organized in two layers, the first using algebraic transitions systems (no failures),
the second ASMs (which adds syntactic ASM rules and failures). The two following sections
describe the specifications of each layer.
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)).
Used basic libraries:
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.
[Imprint]
[Data Privacy Statement]
[E-Mail]