Français Anglais
Accueil Annuaire Plan du site
Home > Collaborations > Collaborations
Collaboration with System X FSF
(since Jan 2013)
This thesis "Automated Generation of Timed Tests with Isabelle and HOL-TestGen" attempts to apply “proof-based testing techniques” [BW12b, BKLW10, BW12a, Fel12] on concrete embedded real-time systems to be concretized by project partners. The Isabelle/HOL-TestGen-system (a plugin in Isabelle/HOL) will be used to formalize wide-spread specification languages (UML,OCL, SysML, Scade) as logical embeddings and to extend them by techniques to generate tests from models involving real-time constraints, currently used in distributed and massively parallel processors. Particular emphasis will be put on integration of vizualization techniques to be integrated into the plateform Isabelle/PIDE underlying HOL-TestGen.

Research activities:                                                    > Publications
  ° Formalisation of (Specification and Programming) Languages in Proof Assistants
  ° Formal Model-Based Testing

  ° Verification of Algorithms, Languages and Systems

  WOLFF Burkhart

More information: