Publications

Liste de publications effectuées par ou avec la participation des ingénieurs de Systerel.

2019

  • Camille Parillaud, Yoann Fonteneau, and Fabien Belmonte. Interlocking formal verification at alstom signalling. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification - Third International Conference, RSSRail 2019, Lille, France, June 4-6, 2019, Proceedings, 215–225. 2019. doi:10.1007/978-3-030-18744-6_14.
    [abstract▼] [BibTeX▼]

2018

  • C Metayer, P Humbert, and PA Brameret. Vers une implémentation sûre et cybersécurisée du protocole opc ua. In Congrès Lambda Mu 21,« Maîtrise des risques et transformation numérique: opportunités et menaces ». 2018.
    [abstract▼] [BibTeX▼]
  • Ning Ge, Arnaud Dieumegard, Eric Jenn, and Laurent Voisin. Correct-by-construction specification to verified code. Journal of Software: Evolution and Process, 30(10):e1959, 2018.
    [abstract▼] [BibTeX▼]
  • Frédéric Badeau, Vincent Lacroix, Vincent Monfort, Laurent Voisin, and Christophe Métayer. Modelling dynamic data structures with the b method. In International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, 420–424. Springer, 2018.
    [abstract▼] [BibTeX▼]
  • Yamine Aït Ameur, Idir Aït-Sadoune, P. Casteran, J. Paul Gibson, Kahina Hacid, Souad Kherroubi, Dominique Méry, Linda Mohand-Oussaïd, Neeraj Kumar Singh, and Laurent Voisin. On the importance of explicit domain modelling in refinement-based modelling design. experiments with event-b. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings, 425–430. 2018. doi:10.1007/978-3-319-91271-4_35.
    [abstract▼] [BibTeX▼]

2017

  • Thai Son Hoang, Laurent Voisin, A. Salehi, Michael J. Butler, Toby Wilkinson, and N. Beauger. Theory plug-in for rodin 3.x. CoRR, 2017. arXiv:1701.08625.
    [abstract▼] [BibTeX▼]

2016

  • Mathieu Clabaut, Ning Ge, Nicolas BRETON, Eric Jenn, Rémi Delmas, and Yoann Fonteneau. Industrial Grade Model Checking Use Cases, Constraints, Tools and Applications. In 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016). TOULOUSE, France, January 2016. URL: https://hal.archives-ouvertes.fr/hal-01291365.
    [abstract▼] [BibTeX▼]
  • Ning Ge, Arnaud Dieumegard, Eric Jenn, and Laurent Voisin. From event-b to verified c via hll. CoRR, 2016. arXiv:1610.07410.
    [abstract▼] [BibTeX▼]
  • Ning Ge, Eric Jenn, Nicolas Breton, and Yoann Fonteneau. Formal verification of a rover anti-collision system. In Critical Systems: Formal Methods and Automated Verification - Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, Pisa, Italy, September 26-28, 2016, Proceedings, 171–188. 2016. doi:10.1007/978-3-319-45943-1_12.
    [abstract▼] [BibTeX▼]
  • Nicolas Breton and Yoann Fonteneau. S3: proving the safety of critical systems. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification - First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings, 231–242. 2016. doi:10.1007/978-3-319-33951-1_17.
    [abstract▼] [BibTeX▼]

2015

  • Marielle Petit-Doche, Nicolas Breton, Roméo Courbis, Yoann Fonteneau, and Matthias Güdemann. Formal verification of industrial critical software. In Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings, 1–11. 2015. doi:10.1007/978-3-319-19458-5_1.
    [abstract▼] [BibTeX▼]

2014

  • Robert Abo, Laurent Voisin, Steve Counsell, and Manuel Núñez. Formal Implementation of Data Validation for Railway Safety-Related Systems with OVADO, pages 221–236. Springer International Publishing, Cham, 2014. doi:10.1007/978-3-319-05032-4_17.
    [abstract▼] [BibTeX▼]
  • Mathieu Clabaut. Formal verification of data for parameterized systems. Formal Methods Applied to Industrial Complex Systems, pages 115–135, 2014. doi:10.1002/9781119004707.ch5.
    [abstract▼] [BibTeX▼]
  • Christophe Metayer, François Bustany, and Mathieu Clabaut. Pragmatic use of b: the power of formal methods without the bulk. Formal Methods Applied to Complex Systems: Implementation of the B Method, pages 187–200, 2014. doi:10.1002/9781119002727.ch7.
    [abstract▼] [BibTeX▼]
  • Laurent Voisin and Jean-Raymond Abrial. The rodin platform has turned ten. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings, 1–8. 2014. doi:10.1007/978-3-662-43652-3_1.
    [abstract▼] [BibTeX▼]
  • David Déharbe, Pascal Fontaine, Yoann Guyot, and Laurent Voisin. Integrating SMT solvers in Rodin. scp, 94(P2):130–143, 2014. doi:10.1016/j.scico.2014.04.012.
    [abstract▼] [BibTeX▼]

2012

  • David Déharbe, Pascal Fontaine, Yoann Guyot, and Laurent Voisin. Smt solvers for rodin. In International Conference on Abstract State Machines, Alloy, B, VDM, and Z, 194–207. Springer, 2012.
    [BibTeX▼]
  • Frédéric Badeau and Marielle Doche-Petit. Formal data validation with event-b. CoRR, 2012. arXiv:1210.7039.
    [abstract▼] [BibTeX▼]

2010

  • Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. Rodin: an open toolset for modelling and reasoning in event-b. International Journal on Software Tools for Technology Transfer, 12(6):447–466, 2010. doi:10.1007/s10009-010-0145-y.
    [abstract▼] [BibTeX▼]
  • Mathieu Clabaut, Christophe Metayer, and Eric Morand. Formal data validation — formal techniques applied to verification of data properties. Embedded Real Time Software and Systems ERTS, 2010.
    [abstract▼] [BibTeX▼]

2009

  • Jean-Raymond Abrial, Christophe Metayer, and Laurent Voisin. Rodin manual and language definition. 2009.
    [BibTeX▼]

2008

  • Christophe Metayer and Mathieu Clabaut. Dir 41 case study. In International Conference on Abstract State Machines, B and Z, 357–357. Springer, 2008. doi:10.1007/978-3-540-87603-8_44.
    [abstract▼] [BibTeX▼]
  • Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, and Laurent Voisin. A roadmap for the rodin toolset. In Abstract State Machines, B and Z, First International Conference ABZ 2008, 347. September 2008. URL: https://eprints.soton.ac.uk/266769/.
    [BibTeX▼]

2007

  • Mathieu Clabaut. A tool for firewall administration. In B 2007: Formal Specification and Development in B, 7th International Conference of B Users, Besançon, France, January 17-19, 2007, Proceedings, 255–256. 2007. doi:10.1007/11955757_22.
    [abstract▼] [BibTeX▼]

2006

  • Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, and Laurent Voisin. An open extensible tool environment for Event-B. In ICFEM, 588–605. 2006.
    [BibTeX▼]

2005

  • Frédéric Badeau and Arnaud Amelot. Using B as a high level programming language in an industrial project: roissy VAL. In ZB 2005, 334–354. 2005. doi:10.1007/11415787_20.
    [abstract▼] [BibTeX▼]
  • C. Métayer, J.-R. Abrial, and L. Voisin. Event-B Language. Technical Report Deliverable 3.2, EU Project IST-511599 - RODIN, May 2005. http://rodin.cs.ncl.ac.uk.
    [BibTeX▼]

2004

  • Frédéric Badeau, Didier Bert, Sylvain Boulmé, Christophe Métayer, Marie-Laure Potet, Nicolas Stouls, and Laurent Voisin. Adaptabilité et validation de la traduction de b vers c. points de vue et résultats du projet bom. Technique et Science Informatiques, 23(7):879–903, 2004.
    [abstract▼] [BibTeX▼]

2003

  • Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, and Laurent Voisin. Adaptable translator of b specifications to embedded c programs. In FME, 94–113. 2003.
    [abstract▼] [BibTeX▼]