The approach Focus on Isabelle introduces a
coupling of the specification framework FOCUS with the
verification system Isabelle/HOL.
Given a system, represented in a formal
specification framework, one can verify its properties
by translating the specification to a HigherOrder
Logic and subsequently using the theorem prover
Isabelle/HOL or the point of disagreement will be
found. Moreover, using this approach one can validate
the refinement relation between two given systems, as
well as make automatic correctness proofs of syntactic
interfaces for specified system components. The
approach uses particularly the idea of refinementbased
verification, where a verification of system properties
can be treated as a validation of a system
specification with respect to the specification of the
properties.
A mapping of operators in FOCUS to the corresponding
definitions in HOL alone is not sufficient for the
method to become easy. Because of this, we also need a
specification and proof methodology. The main point in
our methodology is an alignment on the future proofs to
make them simpler and appropriate for application not
only in theory but also in practice. For this we have
performed a number of case studies, whose results have
helped us to find out different problem points (like
representation of mutually recursive functions,
specification replications, sheaves of channels, a
large number of re nement layers, etc.) and
corresponding solutions for the coupling FOCUS and
Isabelle/HOL. The proofs of some system properties can
take considerable (human) time since the Isabelle/ HOL
is not fully automated. But considering the framework
Focus on Isabelle we can influence on the
complexity of proofs already doing the specification of
systems and their properties, e.g. modifying
(reformulating) specification to simplify the
Isabelle/HOL proofs for a translated FOCUS
specification. Thus, the specification and
verification/validation methodologies are treated as a
single, joined, methodology with the main focus on the
specification part.
For more details please take a look on the publications.
