Completeness of ASM Refinement and IO automata refinement
This page documents the KIV specifications of the completeness proof for ASM refinement
and for IO automata as described in G. Schellhorn: Completeness of ASM Refinement, ENTCS 2008.
The specifications and proofs for ASMs are organized in two layers.
The first layer gives a completeness proof for arbitrary transition systems.
This layer is purely algebraic. The second layer specializes the systems
to be ASMs, where transitions are given by ASM rules. Such rules may fail,
which is expressed using a bottom element algebraically and
as non-termination in wp-calculus and Dynamic Logic (using ASM rules
as programs). The following three sections describe the two layers for ASMs and
the completeness proof for IO automata.
To get an overview over the structure of the specifications of the first layer you can have a look
at the
development graph of the first layer. We describe the important specifications bottom-up:
- The project starts with a simple definition of
transition systems, consisting of initial states and a step relation. Final
states are those, which are not in the domain of the step relation.
- trace-EF-AF defines traces
and the temporal operators EF and AF needed to express the proof obligations
of generalized forward simulations. This specifications uses a definition of
streams
(finite and infinite sequences of elements) from
the library.
- Specification forward
defines the proof obligations
for generalized forward simulation and forward-is-refine shows
that these imply refinement (a form of trace inclusion modulo a relation IO).
- The completeness proof for such systems first defines for every transition system
another deterministic
transition system, which guesses full runs
of the originals system.
It is proved
that this new system has the same finite as well as infinite traces as the original system
- Second, it is shown that any
deterministic concrete system, that refines an abstract system
can be verified
with the generalized forward simulation
R defined here.
- Finally, the concrete system of the second step is instantiated with the system guessing runs from the first step.
This proves completeness: every refinement can be verified by first guessing runs, and then
proving a generalized forward simulation.
The structure of the specifications of the second layer is also visualized by a
development graph, and again we describe the important specifications:
- The second layer first gives an abstract definition of an abstract state machine, which consists of initial and final states together with an (unspecified) ASM rule STEP#. Compared to the presentation of the paper, the ASM has an extra input parameter, that is not changed by the ASM rule (in compiler verification this is useful to model the compiled program, that is interpreted).
- Since ASM rules may fail (or equivalently: diverge)
predicates "maydiverge" and "diverges" are defined
that characterize possible and guaranteed failure using wp-calculus.
- wp-calculus is also used to define (higher-order) predicates
- AFp(s,p)
(every trace starting with s will reach a state where predicate p holds or diverge),
- AFn(s,p) (every trace will reach a state where p holds) and
- EFn(s,p)
(there is a trace that will reach a state where p holds)
here
and to define traces. Note that predicate "isdtrace" characterizes streams that are either infinite or finite. Finite ones
either end with a final state or with a state where the next rule may diverge.
- Operators AFp, AFn, EFn are used in the definition of
generalized forward simulation between two ASMs.
- Generalized forward simulation is proven
to imply
ASM refinement. The proof is done by using of an instance of the generic theory of transition systems:
-
First, an instance of transition systems is defined, where the next state relation is
generated by
embedding an ASM rules
into states with bottom (for nontermination) is defined (the semantics of the ASM rule).
Predicate "maydiverge" is used to characterize a possible bottom result.
- This ASM instance of transition systems gives an instance of the proof, that generalized
forward simulation implies refinement for transition systems. It is now
proven
that the proof obligations for generalized forward simulation between ASMs
and the generalized forward simulation for this instance of transition systems
are equivalent. The proof is similar to proofs in data refinement that also
remove the bottom element from the proof obligations.
- Finally, in specification
ASMforward-is-ASMrefine it is shown, that refinement for this instance
of transition systems implies ASM refinement. This completes the proof.
- To prove completeness of ASM refinement, a direct proof is given, that is similar to the
one for transition systems. Again, the first step is to define for every ASM
a deterministic ASM
which guesses full runs and to
prove
that both have the same finite as well as infinite traces.
- Second, it is shown that any
deterministic concrete ASM, that refines an abstract ASM
can be verified
with the generalized forward simulation
R defined here.
- Finally, the concrete system of the second step is instantiated with the system guessing runs from the first step.
This proves completeness: every ASM refinement can be verified by first guessing runs, and then
proving a generalized forward simulation.
Specifications for IO automata also form a development graph. The content of the theories is:
- A definition of an
IO automaton, consisting of start states and a step relation, that is labelled with
actions (which include an internal action \tau).
- Specification IOtrace
defines fragments, executions and (action) traces. The definitions are as in the original paper
"Forward and Backward Simulations -- Part I: Untimed systems" by N. Lynch and F. Vaandrager,
except that alternating sequences s0, a0, s1, ... are replaced by two
sequences s0, s1, ... and a0, a1, ... (where, for finite ones, the first is one longer than the second)
- IOrefine-def gives the
two refinement definitions "\leq*_T" and "\leq_T",
IOforward
defines forward simulations, and
IOforward-is-leqrefine
proves that the second, stronger definition of refinement is implied by a forward simulation.
- The completeness proof then again proceeds similar to the ones for transition systems and for ASMs.
First, for every IO automaton a
deterministic IO automaton, which guesses the full runs of the original one
is constructed.
IOinfguess-has-same-traces
proves that this deterministic IO automaton has indeed the same finite as well as infinite (action)
traces as the original one.
- Second, it is shown that any
automaton with deterministic steps, that refines an abstract automaton
can be verified
using a forward simulation (defined as a suitable instance of R in the mapping).
- Finally, the concrete system of the second step is instantiated with the automaton guessing runs from the first step.
This proves completeness: every IO automata refinement can be verified by first guessing runs, and then
proving a forward simulation.
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]