Publications

List of publications written by or with the help of Systerel engineers.

2023

  • O. Gilles, D. Gracia Pérez, P.-A. Brameret, and V. Lacroix. Securing iiot communications using opc ua pubsub and trusted platform modules. Journal of Systems Architecture, 134:102797, 2023. URL: https://www.sciencedirect.com/science/article/pii/S138376212200282X, doi:https://doi.org/10.1016/j.sysarc.2022.102797.
    [abstract▼] [full text] [BibTeX▼]

2022

  • Frédéric Badeau, Julien Chappelin, and Joris Lamare. Generating and verifying configuration data with ovado. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: 4th International Conference, RSSRail 2022, Paris, France, June 1–2, 2022, Proceedings, 143–148. Berlin, Heidelberg, 2022. Springer-Verlag. doi:10.1007/978-3-031-05814-1_10.
    [abstract▼] [BibTeX▼]
  • Guignard Anaïs, Alain Ourghanlian, Niguez Julien, Nicolas Systerel Breton, and Vincent Pouzol. Back-to-Back Testing : méthodes formelles pour maîtriser la conformité des implémentations logicielles. In Congrès Lambda Mu 23 “ Innovations et maîtrise des risques pour un avenir durable ” - 23e Congrès de Maîtrise des Risques et de Sûreté de Fonctionnement, Institut pour la Maîtrise des Risques. Paris Saclay, France, October 2022. URL: https://hal.science/hal-03878473.
    [abstract▼] [full text] [BibTeX▼]

2021

  • Nicolas Breton. High Level Language - Syntax and Semantics - Logical Foundation Document. Technical Report C672 pr4.0 rc1 A, Systerel, September 2021. URL: https://hal.science/hal-03356342.
    [abstract▼] [full text] [BibTeX▼]

2020

  • Thai Son Hoang, Laurent Voisin, and Michael Butler. Domain-specific developments using rodin theories. In Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems, pages 19–37. Springer, 2020. doi:10.1007/978-981-15-5054-6_2.
    [abstract▼] [BibTeX▼]
  • Michael Butler, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. The first twenty-five years of industrial use of the b-method. In International Conference on Formal Methods for Industrial Critical Systems, 189–209. Springer, 2020. doi:10.1007/978-3-030-58298-2_8.
    [abstract▼] [BibTeX▼]

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▼] [full text] [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▼]
  • Julien Ordioni, Nicolas Breton, and Jean-Louis Colaço. HLL v.2.7 Modelling Language Specification. Other STF-16-01805, RATP, May 2018. URL: https://hal.archives-ouvertes.fr/hal-01799749.
    [abstract▼] [full text] [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▼]
  • Ning Ge, Arnaud Dieumegard, Eric Jenn, Bruno d’Ausbourg, and Yamine Aït-Ameur. Formal development process of safety critical embedded human machine interface systems. In TASE (11th International Symposium on Theoretical Aspects of Software Engineering), pp. 1–8. Sophia Antipolis, France, September 2017. URL: https://hal.archives-ouvertes.fr/hal-01740640.
    [abstract▼] [full text] [BibTeX▼]
  • Arnaud Dieumegard, Ning Ge, and Eric Jenn. Event-B at Work: Some Lessons Learnt from an Application to a Robot Anti-collision Function. In 9th International Symposium on NASA Formal Methods (NFM 2017), volume 10227 of NASA Formal Methods 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings, 312–341. Moffet Field, CA, United States, May 2017. URL: https://hal.archives-ouvertes.fr/hal-01535060, doi:10.1007/978-3-319-57288-8\_24.
    [abstract▼] [full text] [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▼] [full text] [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▼]
  • Vincent Monfort. Middleware for a distributed and hot-redundant software in ada 2012. ADA USER, 37(4):207, 2016. URL: https://www.systerel.fr/wp-content/uploads/2017/01/AUJ_middleware_A_published.pdf.
    [abstract▼] [BibTeX▼]
  • Nadezhda Baklanova, Jon Haël Brenas, Amani Makhlouf, Christian Percebois, Martin Strecker, and Hanh Nhi Tran. Coding, Executing and Verifying Graph Transformations with small-tALCQe. In International Workshop Graph Computation Models, Part of STAF 2016 (GCM 2016), 1–15. Vienna, Austria, July 2016. URL: https://hal.archives-ouvertes.fr/hal-02879713.
    [abstract▼] [full text] [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.
    [abstract▼] [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. doi:10.3166/tsi.23.879-903.
    [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. doi:10.1007/978-3-540-45236-2_7.
    [abstract▼] [BibTeX▼]