burkhart.wolff

My research interests are in the field of modeling and model-based software development as well as quality assurence by validation and verification. In particular, my research has been focussed on the integration of formal foundations and proof techniques into the model-driven engineering approach (MDE) and model-based testing techniques into software development. This captures the foundation of specification and programming languages and the construction of correct tools - based on interactive and automated theorem proving techniques - in order to support these activities during design, verification and systematic test.

Particular application fields of these techniques have been models of security mechanisms and (more recently) operating systems.

Generally speaking, I believe in Unity within Computer Science - we should strive for a few principles and tools to solve the problems ahead instead diving into a myriad of local techniques. On the other hand, I believe in the importance of experiments, case studies and prototypical tool implementations: Otherwise, we will never know when theoretical principles are really well-chosen. There are enough impressing theoretical stunts out there, nicely published, but without any value...

• Recently, the proposal for the HOL-TestGen-XT project was accepted as part of the "Chair d'excellence" program of the University Paris-Sud. (See also the "official" project web page). The ultimate goal of this research proposal is to extend the realm of feasible state-spaces for HOL-TestGen system (see below) by 4 orders of magnitude - thus offering even more potential for industrial applications in realistic model-based test-scenarios. We suggest a combination of 3 techniques to achieve this goal:
  
  1. We will combine HOL-TestGen with reasonably integrated and configured automated provers from the SAT solver system family, in particular Z3.
  2. With increasing complexity, there will always remain unresolvable constraints. We will use new Isabelle code-generators to convert constraint-systems of unknown logical status into optimized random test code.
  3. In our experience, the success depends substantially on derived rules from the test domain that help to detect unsatisfiable test-cases early. We will explore ways to derive such forms of domain-specific simplification rules can be automated.
  4. We engage in the development of a new GUI for HOL-TestGen in order to meet increasing demands for usability of model-based testing tools. We will actively engage in the PIDE project.


• I am initiator of the project MBT-SEC, funded by British-Telecom (see Project Page). The goal is to use Security policies as model-based specifications for system behaviour and to derive test-cases for them. Currently, the approach has been used to automatically generate test-cases from firewall policies; at present, we are investigating security policies for the core-componants (the "spine") of the patient data-management system for the British-Healthcare-System. I serve as senior researcher and co-supervisor of Lukas Brügger (ETH Zürich). Budget 360000 CHF. (Started in Sept. 2007).

• I was invited researcher in the FSE group (headed by Dr. Wolfram Schulte) at Microsoft Research, Redmond, USA. I investigated ways of an extension of the existing Boogie-Codeverification Tool for the programming language C with interactive proof techniques supported by Isabelle/HOL. With the new Isabelle/HOL backend of Boogie, I was able to prove some challenge problems that could not be proven automatically. I was able to integrate a verified C memory model into an automated prover used for the discharge of verification conditions generated from annotated C code. The system is used in the Verisoft/HyperVisor project (also funded by the BMBF). I partly continued this work as senior researcher within this project at the University of Saarbrücken. 2007 - 2008.
• As leader of the project "Formal Testing Techniques" (ETH 17301), I developed (together with Achim Brucker) a test-case generation system (HOL-TestGen) which derives from formal specifications in higher-order logic (HOL) concrete test-drivers (in SML) performing black-box, grey-boy and sequence test. Our tool has been applied in quite substantial such as firewall-tests.(See also section "Talks/Tutorials".) 2004 - 2007.
• As project leader of the "Modelling and Verification in UML/OCL" project (ETH 17305), I developed a formal semantics of the object-oriented specification modelling language UML/OCL and implemented it in Isabelle/HOL. This includes the development of first proof calculi and decision procedures for OCL. The overall goal of the project is to ge?nerate from class-diagrams annotated with OCL test cases for compo?nents and subsystems. As local project leader of the EU-IP TrustCoM (ETH13581), I developed (together with Jürgen Doser) a model-driven engineering approach for security in web-based services. 2005 - 2007.
• In a former project, I co-initiated the FSA-project (funded by the Deutsche Forschungsgemeinschaft (DFG)), where the modelling and verification of security architectures and their implementation via concrete security technologies in distributed Client-Server Software systems. As a contribution to the project, I developed a tool (HOL-Z, a conservative embedding of the Z-language in Isabelle/HOL together with special proof support for refinement proofs) and performed a substantial case study on it, namely CVS-Server. Recently, I used HOL-Z for an industrial verification case study in the field of applied computer security. 1999 - 2002

Currently, I am actively developping or maintaining the following tools stemmong from former projects. Sources, examples, documentation and specialized publication lists can be received from the corresponding tool web-sites:

• HOL-TestGen
• HOL-OCL
• HOL-Boogie
• HOL-Z

Former, no longer supported sources can be found on the tool web-sites:

• The HOL-CSP Homepage
• The TAS and IsaWin-Homepage

• International Conference of Software Testing (PC-member 10).
• International Conference on International Conference on Testing Software and Systems (PC-member 10).
• Intl. Conference on Theorem Proving in Higher-Order Logics' (TPHOLs): (Co-Chair 03; PC-member 04-08)
• International Conference on Testing of Communicating Systems and Formal Approaches to Testing of Software (TestCom-Fates): (PC-member 05 - 09)
• International Conference on Test and Proof (TAP 2008): (PC-member 08)
• Formal Approaches to Testing and Runtime Verification (Co-Chair 06)
• International Workshop on Formal Methods in Education and Teaching (FMET 08): (PC-member 08)
• OCL Workshop at the UML/MoDELS Conferences: (PC-member 06, 08, 09)
• User Interfaces for Theorem Provers (UITP) (PC-member 05, 06, 10)
• GI-Fachgruppe "Formale Methoden und Software Engineering für Sichere Systeme" (FomSESS): (STC-member 02-08)

• International Conference on Functional Programming (ICFP 2008): (Ref)
• International Joint Conference on Automated Reasoning (IJCAR 2008): (Ref)
• Journal STVR 2008: (Ref)
• Conference of Automated Deduction (CADE 2007): (Ref)
• Formal Methods Europe (FME 2000, 2002, 2005): (Ref)
• 12th International Conference on Logic for Programming Artificial Intelligence?and Reasoning (LPAR 05): (Ref)
• Foundations of Software Science and Computation Structures (FOSSACS 05: (Ref)
• 2nd IEEE International Conference on Software Engineering and Formal Methods (SEFM 04): (Ref)
• 3rd International Conference on Quality Software (QSIC 2003): (Ref)
• Frontieres in Combining Systems (FroCoS 1998, 2000): (Ref)
• ... and refereeing in numerous workshops.

1. Project "MBTSEC" with ETH Zürich (Computer Security headed by David Basin) and British Telecom (contact: Dr. Paul Kearney). See above.
2. Collaboration with the Verisoft-Project (Universität Saaarbrücken, Computer Architecture Group headed by Wolfgang Paul) on Verification and Test of Operating Systems.
3. PIDE Task-Force with TU-München (Isabelle-Group headed by Tobias Nipkow) and University Tübingen, Germany, on future GUI designs for massive parallel formal development tools.

• Matthias Krieger (Uni Paris-Sud, started Sept. 2009)
• Lukas Brügger (ETH Zürich, started Sept. 2007)
• Achim Brucker (ETH Zürich, finished Feb. 2007): An Interactive Proof Environment for Object-Oriented Specifications.
• Thomas Meyer (Universität Bremen, finished 2005): A Framework for Formal Representation and Transformational Optimization of Executable Specifications.
• Rimvydas Rukas (Abo Akademi University, Finland, 2004): Formal Development of Concurrent Components. (Role: External Referee).
• Haykal Tej (Universität Bremen, finished 2003): CSP in Isabelle/HOL.
• Kolyang (Universität Bremen, finished 1997): An Integrated Formal Support Environment for Z in Isabelle/HOL.