Virginie Wiels

Département Traitement de l'information et Systèmes (DTIS)

Director

 

Research domain

Formal methods for the verification of critical embedded software and systems.

  • Combination of static and dynamic analyses of software
  • Software Certification (DO-178C and DO-333)

Training on formal methods at College de Polytechnique (in French)

 

Conferences
 

  • Member of the editorial board for LITES (Leibniz Transactions on Embedded Systems)
  • Forum Méthodes Formelles FMF - Cycle de conférences (in French)
  • PC member of
    • FASE 2017
    • NFM 2017

 

Contact

ONERA/DTIS - Centre de Toulouse

2 avenue Edouard Belin, BP 74025, 31055 Toulouse cedex, France

33 5 62 25 26 57

Virginie.Wiels at onera.fr

,

Publications

2016

  • Pierre Bieber, Frédéric Boniol, Guy Durrieu, Olivier Poitou, Thomas Polacsek, Virginie Wiels, Ghilaine Martinez. MIMOSA: Towards a model driven certication process. ERTS 2016.
  • Antoine Ferlin, Philippe Bon, Simon Collart-Dutilleul and Virginie Wiels.Trace analysis from ERTMS engineering. COMPRAIL 2016.
  • Antoine Ferlin, Virginie Wiels and Philippe Bon. Statistical automaton for verifying temporal properties and computing information on traces. International Journal of Computers Communications and Control, 2016.

2015

  • K. Cabrera Castillos, H. Waeselynck, V. Wiels. Show Me New Counterexamples: A Path-Based Approach. IEEE International Conference on Software Testing, Verification and Validation (ICST) 2015.
  • A. Guduvan, H. Waeselynck, V. Wiels, G. Durrieu, Y. Fusero, M. Schieber. Test Languages for In-the-Loop Avionics Tests. AIAA Journal of Aerospace Information Systems. 2015.
  • Antoine Ferlin, Philippe Bon, Virginie Wiels and Simon Collart-Dutilleul. Vérification parallélisée de propriétés temporelles sur des traces d'exécution, par analyse dynamique formelle. AFADL 2015.
  • Thomas Polacsek, Virginie Wiels and Frédéric Boniol. Une argumentation pour des exigences temps réel. AFADL 2015.
  • Antoine Ferlin, Philippe Bon, Simon Collart-Dutilleul and Virginie Wiels. Parallel verification of temporal properties using dynamic analysis. IESM 2015.

  • Darren Cofer, Gerwin Klein, Konrad Slind, and Virginie Wiels. Qualification of Formal Methods Tools. Report from Dagstuhl Seminar 15182

2014

  • A. Sabas, S. Shankar, V. Wiels, J-J.Ch.Meyer, and M. Boyer. An algebraic approach for the specification and the verification of aspect oriented systems. Book chapter In I. Ghani,W. M. NasirWan Kadir, and M. Nazir Ahmad, editors, Handbook of Research on Emerging Advancements and Technologies in Software Engineering, pages 148–174. IGI Global (Information Science Publishing), 2014.

  • Virginie Wiels. A formal experiment to assess the efficacy of certification standards. AESSCS workshop, Newcastle upon Tyne, May 2014.

  • Frédéric Boniol and Virginie Wiels. Towards modular and certified avionics for UAV. Aerospace lab journal, issue 8 on Aerial robotics, 2014.

 

2013

  • Anthony Fernandes Pires, Thomas Polacsek, Virginie Wiels, Stéphane Duprat. Behavioural Verification in Embedded Software, from Model to Source Code. MODELS 2013.

  • Anthony Fernandes Pires, Thomas Polacsek, Virginie Wiels, Stéphane Duprat. Vérifier le comportement du code d'un système embarqué à partir de son modèle. Journal Européen des Systèmes Automatisés, 47(1-3): 61-75, 2013.

  • Yannick Moy, Emmanuel Ledinot, Hervé Delseny, Virginie Wiels, Benjamin Monate. Testing or Formal Verification: DO-178C Alternatives and Industrial Experience, IEEE Software, 2013.

  • Virginie Wiels, Pierre Bieber, Frédéric Boniol,  Rémi Delmas, David Doose, Guy Durrieu, Olivier Poitou, Thomas Polacsek, Vincent Louis, Florian Many, Ghilaine Martinez. The MIMOSA frame of reference for the certification of military embedded modular architectures. Congrès OTAN/IST "Architecture Definition & Evaluation".

  • Alexandru-Robert Guduvan, Helene Waeselynck, Virginie Wiels, Guy Durrieu, Yann Fusero and Michel Schieber A Meta-model for Tests of Avionics Embedded Systems. MODELSWARD 2013.
  • Alexandru-Robert Guduvan, Helene Waeselynck, Virginie Wiels, Guy Durrieu, Yann Fusero and Michel Schieber. STELAE – A Model-Driven Test Development Environment for Avionics Systems. ISORC 2013.

     

2012

  • Arsène Sabas and Subash Shankar and Virginie Wiels and Michel Boyer. Undesirable Aspect Interactions: A Prevention Policy for Three Aspect Fault Types. SERE 2012 (companion)
  • Antoine Ferlin and Virginie Wiels. Combination of Static and Dynamic Analyses for the Certification of Avionics Software. ISSRE Workshops (WoSoCER 2012).
  • Antoine Ferlin and Virginie Wiels. Calcul de points d'observation pour l'analyse dynamique de programmes. AFADL 2012.
  • V. Wiels, R. Delmas, D. Doose, P.-L. Garoche, J. Cazin, G. Durrieu. Formal Verification of Critical Aerospace Software. Aerospace Lab Journal, Issue 4, May 2012.



     

2011

  • DO-178. Software Considerations in Airborne Systems and Equipment Certification. RTCA/EUROCAE, 2011.
  • DO-333. Formal Methods Supplement to DO-178C and DO-278A. RTCA/EUROCAE, 2011.
  • Arsène Sabas and Subash Shankar and Virginie Wiels and Michel Boyer. Undesirable Aspect Interactions: A Prevention Policy. TASE 2011.
  • Arsène Sabas and Subash Shankar and Virginie Wiels and Michel Boyer. A Categorical Modeling Approach of Aspect-Oriented Systems. TASE 2011.

     

2010

  • Paths to property violation: a structural approach for analyzing counter-examples

    Thomas Bochot, Pierre Virelizier, Hélène Waeselynck, Virginie Wiels

    HASE 2010 (High Assurance Systems Engineering)

    Novembre 2010, San Jose, USA.
  • STANCE: un outil d'analyse structurelle de contre-exemples

    Thomas Bochot, Pierre Virelizier, Hélène Waeselynck, Virginie Wiels

    AFADL 2010 (Approches Formelles dans l'Assistance au Développement de Logiciels)

    Juin 2010, Poitiers, France.
  • Guidance for Using Formal Methods in a Certification Context

    Duncan Brown, Hervé Delseny, Kelly Hayhurst, Virginie Wiels

    ERTSS 2010

    May 2010, Toulouse, France
  • Toward a wider use of formal methods for aerospace systems design and verification

    Yamine Ait Ameur, Frédéric Boniol and Virginie Wiels

    International Journal on Software Tools for Technology Transfer (STTT)

    Volume 12, issue 1, 2010

    DOI 10.1007/s10009-009-0131-4

2009

  • Formal verification of avionics software products

    Jean Souyris, Virginie Wiels, David Delmas, Hervé Delseny

    Formal Methods 2009

    November 2009, Eindhoven, Netherlands

     
  • Model checking flight control systems: the Airbus experience

    Thomas Bochot, Pierre Virelizier, Hélène Waeselynck and Virginie Wiels

    ICSE 2009

    May 2009, Vancouver, Canada

     
  • Application du model checking aux commandes de vol : l'expérience Airbus

    Thomas Bochot, Pierre Virelizier, Hélène Waeselynck et Virginie Wiels

    AFADL 2009

    Janvier 2009, Toulouse, France

2008

  • LETO - A Lustre-based Test Oracle for Airbus critical systems

    Guy durrieu, Hélène Waeselynck and Virginie Wiels

    Formal Methods for industrial Critical systems (FMICS) 2008

    September 2008, L'Aquila, Italie

2007

  • Application de techniques formelles à la vérification et  validation de systèmes embarqués

    Virginie Wiels

    Habilitation à Diriger des Recherches, INPT - ONERA/DTIM, Juin 2007
  • Expérimentations de techniques de vérification de propriétés temps réel sur un système de contrôle de train d'atterrissage

    Frédéric Boniol et Virginie Wiels

    Revue de l'électricité et de l'électronique (REE) - numéro 3, mars 2007

 

2006

  • Formal modelling of avionics systems. An approach based on category theory and the EXPRESS modelling language

    Yamine Aït-Ameur, Alexandre Cortier, Rémi Delmas, Virginie Wiels

    ISOLA 06 (International Symposium on Leveraging Applications of Formal Methods, Verification and Validation)

    Cyprus, November 15-19 2006
  • A methodology for automated test generation guided by functional coverage constraints at specification level

    Odile Laurent, Christel Seguin, Virginie Wiels

    ASE 06 (Automated Software engineering), short paper.

    Tokyo, Japan - September 18-22 2006,
  • Un cadre formel pour la spécification multivue de systèmes avioniques

    Yamine Aït-Ameur, Rémi Delmas, Virginie Wiels

    Technique et Science Informatiques, Volume 25 - numéro 1/2006
  • Automated functional test case generation from data flow specifications using structural coverage criteria

    Christel Seguin, Guy Durrieu, Virginie Wiels, Bruno Marre, Benjamin Blanc, Odile Laurent, Abdesselam Lakehal, Ioannis Parissis

    ERTS 06 (Embedded Real-Time Systems)

    January 25-27 2006, Toulouse, France

 

2004

  • Un cadre formel pour la spécification de systèmes avioniques

    Y. Ait Ameur, Rémi Delmas, Virginie Wiels

    AFADL 2004 (Approches Formelles dans l'Assistance au Développement de Logiciels)

    June 16-18 2004, Besançon, France
  • A framework for heterogeneous formal modeling and compositional verification of avionics systems

    Rémi Delmas, Virginie Wiels, Y. Ait Ameur

    MEMOCODE 2004 (Formal Methods and Models for Codesign)

    June 22-25 2004, San Diego, USA
  • Automatic test case generation for critical embedded systems

    Guy Durrieu, Odile Laurent, Christel Seguin, Virginie Wiels

    DASIA 2004 (Data Systems in Aerospace)

    June 28-30 2004, Nice, France
  • Integration of heterogeneous formal techniques for the design of avionics systems

    Yamine Ait-Ameur, Frédéric Boniol, Rémi Delmas, Emmanuel Grolleau, Nathalie Torrecillas, Virginie Wiels

    DASIA 2004 (Data Systems in Aerospace)

    June 28-30 2004, Nice, France
  • Formal proof and test case generation for critical embedded systems using SCADE

    Guy Durrieu, Odile Laurent, Christel Seguin, Virginie Wiels

    IFIP World Computer Congress

    Topical Day on "Emerging tools and techniques for avionics certification"

    August 22-27 2004, Toulouse, France
  • Proceedings of ASE-2004: The 19th IEEE Conference on Automated Software Engineering. IEEE CS Press.

    Virginie Wiels, Kurt Stirewalt, eds.

     November, 2004. Linz, Austria.

 

2003

  • Robustness analysis of avionics embedded systems

    Y. Ait Ameur, G. Bel, F. Boniol, S. Pairault, V.Wiels

    Languages, Compilers and Tools for Embedded Systems LCTES'03

    11-13 juin 2003, San Diego, USA
  • Formalisation catégorique d'un calcul de composants dédié au domaine de l'avionique

    Y. Ait-Ameur, R. Delmas, V. Wiels.

    Formalisation des Activités Concurrentes FAC'03

    12-13 mars 2003, Toulouse, France 
  • Analyse de robustesse de systèmes avioniques

    Y. Ait Ameur, F. Boniol, S. Pairault, V.Wiels

    Journées Francophones des Langages Applicatifs JFLA 03

    27-28 janvier 2003, Chamrousse, France

 

2002

  • Checking Secure Interactions of Smart Card Applets: Extended version

    P. Bieber,  J. Cazin, V.Wiels,  G. Zanon, P. Girard, J-L. Lanet

    Journal of Computer Security vol. 10, Numero 4, 2002, pages 369-398.
  • A component based methodology for description of complex systems. An application to avionics systems

    Y. Ait-Ameur, B. d'Ausbourg, F. Boniol, R. Delmas, V. Wiels

    European Systems Engineering Conference 2002

    21-24 Mai 2002, Toulouse, France
  • Modèles comportementaux pour l'avionique modulaire intégrée

    G. Bel, F. Boniol, G. Durrieu, J. Foisseau, C. Fraboul, V. Wiels

    Logiciels Temps Réel Embarqués 2002

    24-25 Janvier 2002, Toulouse, France

 

2001

  • Using formal verification techniques to reduce simulation and test effort

    O. Laurent, P. Michel, V. Wiels

    Proceedings of FME 2001

    12-16 march, Berlin, Germany
  • Un exemple de modèle conceptuel de référence pour l'ingénierie des systèmes avioniques

    J. Foisseau, V. Wiels, F. Boniol

     Conférence annuelle d'ingénierie système

     26-28 juin 2001, Toulouse, France

 

2000

  • Checking secure interactions of smart card applets

    P.Bieber, J.Cazin, P.Girard, JL.Lanet, V.Wiels, G.Zanon

    Proceedings of Esorics 2000
  • The PACAP prototype: a tool for detecting Java card illegal flow

    P.Bieber, J.Cazin, A. El Marouani, P.Girard, JL.Lanet, V.Wiels, G.Zanon

     Java Card Forum 2000

     Septembre 2000, Cannes, France
  • Detecting illegal information flow using abstract interpretation and model checking

    P.Bieber, J.Cazin, A. El Marouani, P.Girard, JL.Lanet, R. Muller, V.Wiels, G.Zanon

    Gemplus Developer Conference 2000

    Juin 2000, Montpellier, France
  • Certification d'un porte-monnaie electronique

    P.Bieber, J.Cazin, P.Girard, JL.Lanet, V.Wiels, G.Zanon

     Journees FAC 2000

     Mai 2000, Toulouse, France
  • Extended institutions for testing

    M. Doche and V. Wiels

    AMAST 2000

    May 20-27 2000, Iowa City, USA
  • Electronic Purse Applet Certification: Extended Abstract

    P.Bieber, J.Cazin, V.Wiels, G.Zanon, P.Girard, JL.Lanet

     Proceedings of the workshop on security architectures and information flow

     Electronic Notes in Theoretical Computer Science

 

1999

  • Formal modeling of Space Shuttle software change requests using SCR

    V. Wiels and S. Easterbrook

     International Symposium on Requirements Engineering 99

     June 7-11 1999, Limerick, Ireland
  • A modular approach to specify and test an electrical flght control system

    M. Doche, C. Seguin and V. Wiels

    Fourth international workshop on Formal Methods for Industrial Critical Systems

    July 11-12 1999, Trento, Italy

 

1998

  •  Management of evolving specifications using category theory

    V. Wiels and S. Easterbrook

     Automated Software Engineering 98

     October 13-16 1998, Hawai
  • V&V through Inconsistency Tracking and Analysis

    S. Easterbrook, J. Callahan and V. Wiels

    International Workshop on Software Specification and Design

     April 16-18 1998, Ise-Shima, Japan 
  • Module Templates for the Specification of Fault-Tolerant Systems

    M. Doche, J. Cazin, D. Le Berre, P. Michel, C. Seguin, V. Wiels

    DASIA 98

    May 25-28 1998, Athens, Greece

 

1997

  • Assistance au developpement et a la maintenance de logiciels basee sur la composition

    P.Michel, V.Wiels

    Actes des seminaires action scientifique France Telecom

    Logiciels pour les telecommunications, mars 1997.
  • Interaction de formalismes logiques et algebriques. Une etude de cas

    P.Azema, JP. Bahsoun, P.Michel, V.Wiels

    Journees AFADL

    28-29 mai 1997, Toulouse
  • A framework for modular formal specification and verification

    P. Michel, V. Wiels

    Formal Methods Europe 97

    15-19 septembre 1997, Graz
  • Modularite pour la conception et la validation formelles de systemes

    V. Wiels

    Ph.D thesis

    ENSAE, oct 1997

 

1996

  • Un calcul de modules pour combiner les développements ascendants et descendants

    P.Michel, V.Wiels

    Journees Formalisation des Activites Concurrentes LAAS-CNRS

      7-8 fevrier 1996, Toulouse
  • Using a logical and categorical approach for the validation of fault-tolerant systems

    C. Seguin, V. Wiels

    Formal Methods Europe 96

    18-22 mars 1996, Oxford
  • Modular Specification and Validation of Systems

    P.Michel, V.Wiels

    ECOOP Workshop on Proof Theory of Concurrent Object-Oriented Programming

    8 Juillet 1996, Linz

 

1995

  • Un cadre logique et compositionnel pour la conception de systèmes concurrents

    C.Seguin, V. Wiels

    Journees Formalisation des Activites Concurrentes LAAS-CNRS

    4-5 avril 1995, Toulouse
  • Verification experiments on a large fault-tolerant distributed system

    F.Pagani,  C.Seguin,  P.Siron, V. Wiels

    2nd AMAST Workshop on Real-Time Systems

    14-16 juin 1995, Bordeaux (France)
  • Assistance au developpement et a la maintenance de logiciels basee sur la composition: ebauche d'un modele conceptuel

    P.Michel, V.Wiels

      Actes des seminaires action scientifique France Telecom

    Logiciels pour les telecommunications, septembre 1995.

 

1994

Specification et verification de programmes paralleles tolerants aux fautes.

 Virginie Wiels

Master thesis - ENSEEIHT,