Research overview

My research interests are in the field of model-based software development as well as quality assurence by validation and verification. In particular, my research is focussed on the integration of formal foundations and proof techniques into the model-driven software engineering and model-based testing techniques. This comprises work on the semantic foundation of specification and programming languages, the development of calculi for refinement and test-generation as well as the construction of correct tools in order to support these activities during design, verification, systematic test and certification.

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

A a mission, 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.

Ongoing research projects

  • The Isabelle/DOF project (see Tools below).
  • The Isabelle/C project (see Tools below).

Past research projects

  • The project PST Performances des Systemes de Transport (June. 2016 - June. 2019 ). The new generations of transport system equipment must be able to integrate monitoring, communication and optimization functions (cyber security, data collection, energy saving etc.) while at the same time ensuring safe, high performance operation of the basic functions of control/command. In a sub-project called T4, an integrated formal development has been undertaken together with the development of a specific "continuous verification/continuous-build" tool-chain based on Isabelle/HOL. Managing an integrated document, it is designed to assure the global coherence from models, designs, code, tests and thorough documentation of the process targeting formal certification following CENELEC.
  • The EU-Project EUROMILS (Oct. 2012 - Sept. 2015 ). The projects cornerstone is MILS (Multiple Independent Levels of Security), a high-assurance security operating system that supports the coexistence of untrusted and trusted components, based on verifiable separation mechanisms and controlled information flow. For the first time in Europe, EURO-MILS does a complete Common Criteria security evaluation of a MILS system to its highest levels of assurance, including formal verification engineering. Hardware dependencies are addressed from the beginning by prototype development on two hardware platforms in automotive and avionics.
  • The ANR-project Paral-ITP (Nov. 2011 - Apr. 2015) with the Project Partners are INRIA Roquencourt (Hugo Herbelin), INRIA Saclay (Bruno Barras) and U-PSud/LRI (B.Wolff, Project Leader).
    Interactive theorem proving is a technology of fundamental importance for mathematics and computer-science. It is based on expressive logical foundations and implemented in a highly-trustable way. Applications include huge mathematical proofs and semi-automated test-case generation procedures for complex software systems. Interactive development of larger and larger proofs increases the demand for computing power, which means explicit parallelism on current multi-core hardware.
    Both Coq and Isabelle have elaborated the prover architecture over the years, driven by the demands of sophisticated proof procedures, derived specification principles, large theory libraries etc. Despite this success, the operational model of interactive proof checking is largely limited by sequential ML evaluation and the sequential read-eval-print loop, as inherited from LCF.
    The proposed project intends to overcome the sequential model both for Coq and Isabelle, to make the resources of multi-core hardware available for even larger proof developments. Beyond traditional processing of proof scripts as sequence of proof commands, and batch-loading of theory modules, there is a large space of possibilities and challenges for pervasive parallelism. This affects many layers of each prover system: basic computational structures, inference kernel, tactical programming, proof command language, and interactive front-ends.
  • The HOL-TestGen-XT project (2009-2012) 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 was to extend the realm of feasible state-spaces for HOL-TestGen system (see below) by several orders of magnitude - thus offering even more potential for industrial applications in realistic model-based test-scenarios. We suggest a combination of 5 techniques, namely SMT-solver integration for test-data selection, the use of new code-generators, the exploit of parallel execution of normal-form computations in multi-core architectures, domain-specific technologies.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 actively engaged in the PIDE project. Here is the final project report
  • I was initiator of the project MBT-SEC, funded by British-Telecom (2007-2010; see Project Page). The goal was 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 were investigating security policies for the core-componants (the "spine") of the patient data-management system for the British-Healthcare-System. I served as senior researcher and co-supervisor of Lukas Brügger (ETH Zürich). Budget 360000 CHF.
  • 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.

Tools

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

Collaborations

  1. Project "PST" with IRT SystemX (headed by Francoise Caron,Alstom; , Paul Labrogere SystemX). (Started 169).
  2. Project "FSF" with IRT SystemX (headed by Elie Soubiran,Alstom, Paul Labrogere SystemX) and Inria Saclay (headed by Bruno Barras). (2012-15).
  3. Project "Paral-ITP" with Inria Roquencourt (headed by Hugo Herbelin) and Inria Saclay (headed by Bruno Barras). (Started 2010). See above.
  4. Project "EURO-MILS" with SysGO (headed by Sergey Tverdyshev) and consortium of 10 other partners. (Started 2010). See above.
  5. Project "MBTSEC" with ETH Zürich (Computer Security headed by David Basin) and British Telecom (contact: Dr. Paul Kearney). Finished (2012).See above.
  6. Collaboration with the Verisoft-Project (Universität Saaarbrücken, Computer Architecture Group headed by Wolfgang Paul) on Verification and Test of Operating Systems. (Finished 2011).
  7. PIDE Task-Force with TU-München and University Tübingen, Germany, on future GUI designs for massive parallel formal development tools. (Finished 2010).

Phd Supervisions

  • Hai Nguyen Van (Uni Paris-Sud, finished June 2018)
  • Frederic Tuong (Uni Paris-Sud, finished March. 2017)
  • Romain Aissat (Uni Paris-Sud, finished Dec. 2016)
  • Yakoub Nemouchi (Uni Paris-Sud, finished Dec. 2016)
  • Matthias Krieger (Uni Paris-Sud, finished Dec. 2011) Test Generation and Animation Based on Object-Oriented Specifications.
  • Lukas Brügger (ETH Zürich, started Sept. 2007, finished June 2012). A Framework for Modelling and Testing of Security Policies.
  • 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.
  • 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.