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)

 

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

2018

• César Ochoa Escudero, Rémi Delmas, Thomas Bochot, Matthieu David, Virginie Wiels: Automatic Generation of DO-178 Test Procedures. NFM 2018: 399-415
• Viet-Hoang Le, Loïc Correnson, Julien Signoles, Virginie Wiels:
  Verification Coverage for Combining Test and Proof. TAP 2018: 120-13

2017

• Frédéric Boniol, Virginie Wiels, Yamine Aït Ameur, Klaus-Dieter Schewe:
  The landing gear case study: challenges and experiments. STTT 19(2): 133-140 (2017)

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