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
