Projects and Collaborations

This page lists the research projects and collaborations concerning foundational research in testing or test-tools. This involves research on proof-based test-generation technologies, research to formalize specification formalisms and their integration into generic test-procedures as well as the development specific forms of parallel symbolic computation in order to improve the practicability of the approach.

The research in the application domains results in --- or is partially support by --- a number of funded research projects or voluntary collaborations:

  • Representative Fortesse : Burkhart Wolff (directeur thèse)
  • Members: Delphine Longuet (co-directeur) , Frederic Tuong (doctorand), Elie Soubiran (System X).
  • Funding and type of contract : Thesis inside the Projet FSF (IRT System X, Programme Tools et Technologies, Sous Programme Systèmes Embarqués, Projet Fiabilité et Surete de Fonctionnement (FSF).
  • Partners : IRT System X, Localized at NanoInnov, Palaiseau.
  • Periode : 1.2. 2013 - 31.1.2016  
  • Principal goals :  This thesis "Automated Generation of Timed Tests with Isabelle and HOL-TestGen" attempts to apply “proof-based testing techniques” [BW12bBKLW10BW12aFel12] 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.
  • More on the web: http://www.irt-systemx.fr/
 
  • Representative Fortesse : Burkhart Wolff (site coordinator)
  • Members : Abderachmane Feliach(Post-doc) , Yakoub Nemouchi (doctorand).
  • Funding and type of contract : EU Integrated Project
  • Partners : Sysgo (France & Germany, coord.), Technikon(Austria), OpenSynergy(Germany), Jemm Research(France),  EADS, Airbus(France), Thales (France), DFKI Saarbrücken (Germany), Universiteit Gent(Belgium), Open Universiteit(Netherlands), T-Systems (Germany)
  • Periode : 1.10. 2012 - 30.9.2015 
  • Principal goals :  Secure European virtualisation for trustworthy applications in critical domains. The mission of the EURO-MILS project is to develop a solution for virtualisation of heterogeneous resources and provide strong guarantees for isolation of resources by means of Common Criteria certification with usage of formal methods. ForTesSE is involved in particular as part of the activity to use model-based testing techniques to establish conformance of the real code to the projects system models. Part of the research is oriented to the question, how can tests be organized in a format such that it is useable in an Common Criteria EAL5+ certification process.
  • More on the web: https://www.euromils.eu/
 

ANR Project Paral-ITP

  • Representative Fortesse : Burkhart Wolff (ANR project coordinator)
  • Members: Makarius Wenzel, Delphine Longuet, Frederic Voisin, Pierre Courtieu, Olivier Pons.
  • Funding and type of contract : ANR / System@tic
  • Partners : INRIA Rocquencourt (H. Herbelin), INRIA Saclay (B. Barras), Univ. Paris-Sud / LRI (B. Wolff, coord.)
  • Periode : 1.12. 2011 - 31.3.2015 
  • Principal goals : The proposed project intends to overcome the sequential execution model for the interactive theorem proving systems 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 batchloading 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. Some of these aspects need to be addressed for Coq and Isabelle in slightly different ways, to accommodate different approaches in either system tradition. These substantial extensions of the operational aspects of interactive theorem proving shall retain the trustability of LCF-style proving at the very core. The parallelization mechanisms are of foundational importance for HOL-TestGen, a modeling and test data generation environment based on Isabelle.
  • More on the web: Project Page
 
  • Representative Fortesse : Pascal Poizat 
  • MembersPascal Poizat,Fatiha Zaidi, Huu Nghia Nguyen, 
  • Funding and type of contract : ANR Project.
  • Partners : GENIGRAPH Genigraph, INRIA Institut national de recherche en informatique et en automatique - (Inria siège), IT Institut Telecom - Sud Paris, Montimage Montimage, LRI Universite de Paris XI [Paris-Sud], IRIT Université Toulouse III [Paul Sabatier]
  • Periode : 15.11.2010 - 14.11.2013 
  • Principal goals :   The future Internet will bring a growing number of networked applications (services), devices and individual data (including private ones) to end-users (citizens, consumers, employees). The important challenges are the organization of their access, and the guarantee of trust and privacy.
    The objectives of the PIMI project (Personal Information Management through Internet) are the definition of a model-based design environment and a deployment platform for Personal Information Management System (PIMS).  The future PIMS must provide the end-user personal data access with services that are relevant to his needs. In order to take mobility into account, the PIMS will be accessed both by mobile devices (smartphone) and Internet-connected Personal Computers. 
    With the increasing number of e-services and associated data being accessible through Internet, the number and complexity of PIMS will augment dramatically in the near future. This will require strong research investment in a number of topics, all contributing to the expected usability and accessibility of Individual Information Spaces for the end-user: 
    • Electronic trust and reputation of the services
    • Secured private data transfer between PIMS and between services 
    • Ergonomic Human Computer Interface including mobile ones
    • Service composition and re-composition based on end-users requirements (life events), on e-service trust and runtime feedback  
    • Quality of Service / Quality of Experience self adaptation 
    • Advanced algorithms to monitor the PIMS, the private data and service accesses 
  • Web-Site: PIMI
 

PSUD Project HOL-TestGen-XT

  • Representative ForTesSE : Burkhart Wolff (coordinator)
  • Members : Mathias Krieger (Doctorand), Dr. Makarius Wenzel (Post-doc)
  • Funds and type of contract : Chaire Digiteo / Chaire Univ. Paris-Sud
  • Collaborations : ETH Zürich (Lukas Brugger), SAP (Achim Brucker), BT (Paul Kearney)
  • Time period : 1.3.2009 - 1.3.2012
  • Principal objectives :
    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.
 

Collaboration PIDE

  • Representative Fortesse : Burkhart Wolff
  • Funding and type of contract : Chaire Digiteo + Univ. Paris-Sud.
  • Partners : TU München (Makarius Wenzel), Uni Tübingen (Holger Gast), SAP (Achim Brucker), Univ. Paris-Sud (B. Wolff)
  • Periode : 1.6. 2009 - 1.6.2011
  • Principal goals : The purpose of the \pi-IDE Project (spell: PIDE-Project) is to create an Integrated Development Environment (IDE) for Proofs that brings Interactive Theorem Proof Assistants truly to the rest of us… Our ultimate goal is an IDE that makes interactive theorem proving (ITP) amenable both to high-school education as well as power users in theorem proving, and that makes theorem provers as easy to install as, say, NeoOffice under MacOS, and as common to use as, say, a Computer Algebra System. Furthermore, we want to exploit the full potential of ITP Systems such as Isabelle, Coq or HOL4 as implementation basis for Formal Methods Tools.
  • More on the web: Project Page

 

International Collaboration MoBasT

  • Representative Fortesse : Marie-Claude Gaudel
  • Members: Maire-Claude Gaudel, Abderachmane Felliachi, Burkhart Wolff
  • Funding and type of contract : Royal Society + CNRS
  • Partners : University of York (Ana Cavalcanti), CNRS/LRI (Marie-Claude Gaudel)
  • Periode : 2012 - 2014 
  • Principal goals : This project aims at strengthening and consolidating an existing and fruitful collaboration in the area of software testing based on formal specifications. The considered specifications are in CIRCUS, a language developed in York, which integrates the notions of states and complex data types (in a Z-like style) and communicating parallel processes inspired from CSP. Morover, the language comes with a formal notion of refinement and allows to take into account abstract specifications and their transitions to models of programs. On the bases of the theory of formal software testing and the proof and test generation tools developed in LRI the project will address the following questions:
    • What are the integrated testing strategies applicable to such languages, which combine aspects that have been studied separately, so far, with respect to testing? 
    • What are the integrated testing strategies applicable to such languages, which combine aspects that have been studied separately, so far, with respect to testing?
    • How to justify these strategies and their coherence with the underlying test hypothesis?
    •  How to implement them in a well-founded way, starting from the existing proof and generation tools that exist in York and Orsay
We also want to address the problem of the selection of finite test sets. Since, in the exhaustive test sets, we have a symbolic version of the tests, with labels constraining communicated values, it is natural to consider strategies based on constraints decomposition and solving. We propose as well to go further and address the challenging problem of providing coverage of complex internal data operations, and justify the soundness of the techniques.

 

 
 

British Telecom Project MBT-SEC

  • Representative Fortesse : Burkhart Wolff (coordinator)
  • Funding and type of contract : British Telecom (BT), funding partners at ETH Zürich and travelling funds for Univ. Paris-Sud.
  • Partners : ETH Zürich (David Basin, adm. head), Lukas Brügger (doctorand), BT (Paul Kearney), Univ. Paris-Sud/LRI (B. Wolff, scientific coordinator)
  • Periode : 1.9. 2007 - 31.8.2010
  • Principal goals : 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. B. Wolff serves as senior researcher and co-supervisor of Lukas Brügger (ETH Zürich).
  • More on the web: Project Page
 

Cofecub Project RobustWeb

  • Responsable for ForTesSE : Fatiha Zaïdi
  • Members : Lina Bentakouk (Doctorante), Marie-Claude Gaudel
  • Financing and contract type: Cofecub
  • Partners : LRI - Télécom-Management Sud-Paris (ex INT) - LAAS - UNICAMP (Brésil, leader) - UFES (Frésil) - INPE (Brésil)
  • Duration : 1.09.2008 - 1.09.2010
  • Research Objectives : Construction et validation of SOA applications by web services.
 

ANR Project WebMov

  • Responsible for ForTesSE : Fatiha Zaïdi (Project leader)
  • Members : Lina Bentakouk (Doctorante), Marie-Claude Gaudel, Mounir Lallali(ATER)
  • Financing and contract type : ANR TechLog
  • Partners : LRI - Télécom-Management Sud-Paris (ex INT) - LABRI - SOFTEAM - MONTIMAGE - UNICAMP (Brésil).
  • Duration : 22.11.2007 - 31.08.2010
  • Research Objectives :The main objective of WebMoV is to contribute to the design, composition and validation of Web Services through a high level of abstraction view and aSOA based logical architecture vision. In this domain, industry usually constructs new services by composition of modules which describe existing Web Services. These composition mechanisms are called orchestration. In this proposal, we are interested in the design and composition mechanisms for Web Services as well as their validation using different types of testing techniques.
 

ANR Project Verap

  • Responsible for ForTesSE : Marie-Claude Gaudel
  • Members : Fatiha Zaïdi
  • Financing and contract type : ANR SESUR
  • Partners : LRI - Paris VII.
  • Duration : 2007 - 2010
  • Research Objectives :
Attachments:
Download this file (MoBaST-LRI-York.pdf)MoBaST-LRI-York.pdf[ ]130 Kb
You are here Home