Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat Etranger de WOLFF Burkhart
WOLFF Burkhart
Doctorat Etranger
Equipe :

Professor

Début le 01/01/1970
Direction :

Financement :
Etablissement d'inscription : vide
Lieu de déroulement : Freiburg im Breisgau, Allemagne

Soutenue le 01/01/1970 devant le jury composé de :
Basin, Korvink et al.

Activités de recherche :

Résumé :
The development of tools for program analysis, verification and refinement is a prerequisite for the proliferation of formal methods in industry and research. While most tools were directly implemented in a programming language, the ultimate goal of this work is to represent widely known formal methods in a so-called logical framework by their semantics using a particular representation technique - called shallow embedding - motivated by more efficient deduction. Based on this representation, symbolic computations in tool implementations can be based on formally proven correct derived rules. As such, this correctness-oriented approach has been known for a while and has been criticized for a number of shortcomings:
the application range of embeddings in logical frameworks is limited to very small and artificially designed languages,
their application is impossible when the formal specification method is still under development,
embedding the semantics conservatively and deriving some rules on this basis does not imply that there is a comprehensive support of a method that is technically powerful enough for applications,
the integration in a more global software engineering process and its pragmatics is too difficult, and
the usability of embeddings is doubtful even if one is targeting at the (fairly small market of) proof environments.
In contrast to this criticism, we claim that our approach is feasible. We substantiate this by developing:
suitable embeddings for widely used formal methods, including process-oriented, data-oriented and object-oriented specification methods (CSP, Z, UML/OCL),
abstractions and aspect-oriented structuring techniques allowing for the quick development of semantic variants enabling the study consequences of changes in formal methods under development (like UML/OCL),
particular techniques for generating library theories, for supporting particular deduction styles in proofs, for specialized deduction support for concrete development methodologies,
different scenarios of the integration of the developed tools in conventional tool chains in software engineering, and
front-ends for light-weight integration into tool chains (like HOL-Z 2.0) or prototypic encapsulation of logical embeddings into generic graphical user-interfaces for a more comprehensive encapsulation.
Finally, we validate one of these tool chains (HOL-Z 2.0) by a substantial case-study in the field of computer security.