Informatik
 
  focus

  FOCUS   

       
Overview
 
Publications
 
Projects
 
Case Studies
 
Focus on Isabelle
 
LaTeX representation
 
AutoFocus
 
   
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
   

 

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 Higher-Order 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 refinement-based 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.

 
               focus on isabelle logo

 
 
  Maria Spichkova
  Last modified 29.07.2011