Publications

2024¶

• Thai Son Hoang, Laurent Voisin, Karla Vanessa Morris Wright, Colin Snook, and Michael Butler. Semantics formalisation — from event-b contexts to theories. In ABZ 2024 — 10th International Conference on Rigorous State Based Methods (25/06/24 - 28/06/24). June 2024. URL: https://eprints.soton.ac.uk/490660/.
  [abstract▼] [full text] [BibTeX▼]

  The Event-B modelling language has been used to formalise the semantics of other modelling languages such as Time Mobility (TiMo) or State Chart XML (SCXML). Typically, the syntactical elements of the languages are captured as Event-B contexts while the semantical elements are formalised in Event-B machines. An alternative for capturing a modelling language’s semantics is to use the Theory plug-in to build datatypes capturing the syntactical elements of the language and operators to represent the various semantical aspects of the language. This paper draws on our experience on the statemachines (part of SCXML) to compare the two approaches in terms of modelling efforts.

  @inproceedings{soton490660,
      author = "Hoang, Thai Son and Voisin, Laurent and Wright, Karla Vanessa Morris and Snook, Colin and Butler, Michael",
      booktitle = "ABZ 2024 — 10th International Conference on Rigorous State Based Methods (25/06/24 - 28/06/24)",
      month = "June",
      title = "Semantics formalisation — from Event-B contexts to theories",
      year = "2024",
      keywords = "Statecharts, SCXML, Event-B, Theory Plugin, Semantics Formalisation",
      url = "https://eprints.soton.ac.uk/490660/"
  }
  

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▼]

  In the Industry 4.0 context, data are a valuable asset that must be protected. Ensuring the confidentiality and integrity of the data exchanged by the IIoT devices is challenging, especially when those devices are out of the companies premises or easily accessible (we call them out-premise devices). These devices become primary targets for attackers as a way to compromise data and cause damage to infrastructure or people. OPC UA PubSub provides the appropriate mechanisms to build scalable (e.g. one-to-many) secure and interoperable solutions with end-to-end encryption. However, authentication of IIoT devices remains a sensitive question, as it requires to securely embedding secrets. We present a novel approach based on open source software aiming to secure out-premise devices authentication, enabling the confidentiality and integrity of data exchanges with the rest of the system. Our approach uses a Trusted Platform Module as a secure element to protect the secrets embedded on devices. We further apply the approach on a predictive maintenance use case and evaluate the security level of our solution in such use case.

  @article{GILLES2023102797,
      author = "Gilles, O. and {Gracia Pérez}, D. and Brameret, P.-A. and Lacroix, V.",
      title = "Securing IIoT communications using OPC UA PubSub and Trusted Platform Modules",
      journal = "Journal of Systems Architecture",
      volume = "134",
      pages = "102797",
      year = "2023",
      issn = "1383-7621",
      doi = "https://doi.org/10.1016/j.sysarc.2022.102797",
      url = "https://www.sciencedirect.com/science/article/pii/S138376212200282X",
      keywords = "Security, Authentication, IIoT, OPC UA, PubSub, Security key server, TPM 2.0, MQTT, Railway, ICS"
  }
  

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▼]

  This article presents a novel use of OVADO, a data validation tool for railway systems configuration, and its application in an industrial setting. We describe how OVADO usage evolved from data validation to generation of equipment configuration data, and report on the application of this technique in a real industrial context: the deployment of the OCTYS VTPA system by Alstom on Line 6 of the Paris metro, operated by RATP. While this new method requires some adaptation in industrial processes in order to retain compliance with a SIL4 safety level, it improves translation quality and factorizes data generation and verification activities.

  @inproceedings{RSSRail2022,
      author = "Badeau, Fr\'{e}d\'{e}ric and Chappelin, Julien and Lamare, Joris",
      title = "Generating and Verifying Configuration Data with OVADO",
      year = "2022",
      isbn = "978-3-031-05813-4",
      publisher = "Springer-Verlag",
      address = "Berlin, Heidelberg",
      doi = "10.1007/978-3-031-05814-1\_10",
      booktitle = "Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: 4th International Conference, RSSRail 2022, Paris, France, June 1–2, 2022, Proceedings",
      pages = "143–148",
      numpages = "6",
      keywords = "Railway systems, Ovado, B language, Data validation, CBTC",
      location = "Paris, France"
  }
  

• 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▼]

  B2BT is a process of automatic test sequences generation based on formal methods. These sequences describes the observable behavior of system: for every step, inputs and outputs are given. Outputs values are computed from inputs and memories values. Hence, they are used on a test bench in order to control the compliance of the implementation with the initial model used to generate the sequences. The sequences are designed in order to detect mutations of the implementation that would change the observable behavior of the system. Coverage criteria are given along the B2BT method. Industrial applications based on EDF use case and a railway signaling use case are presented

  @inproceedings{hal03878473,
      AUTHOR = {Ana{\"i}s, Guignard and Ourghanlian, Alain and Julien, Niguez and Breton, Nicolas Systerel and Pouzol, Vincent},
      TITLE = "{Back-to-Back Testing : m{\'e}thodes formelles pour ma{\^i}triser la conformit{\'e} des impl{\'e}mentations logicielles}",
      URL = "https://hal.science/hal-03878473",
      BOOKTITLE = "{Congr{\`e}s Lambda Mu 23 `` Innovations et ma{\^i}trise des risques pour un avenir durable '' - 23e Congr{\`e}s de Ma{\^i}trise des Risques et de S{\^u}ret{\'e} de Fonctionnement, Institut pour la Ma{\^i}trise des Risques}",
      ADDRESS = "Paris Saclay, France",
      YEAR = "2022",
      MONTH = "October",
      KEYWORDS = "preuve formelle ; v{\'e}rification ; validation ; syst{\`e}mes critiques",
      HAL_ID = "hal-03878473",
      HAL_VERSION = "v1"
  }
  

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▼]

  This document provides a formal definition of the modelling language HLL - High Level Language. HLL is a declarative stream-based language supporting a large variety of types and operators. It is suitable for modelling discrete-time sequential behaviors and expressing temporal properties of these behaviors. In 2018 the HLL Forum initiative started as a working group of tool providers and users of HLL. New features of HLL (compared to version 2.7) were developed jointly by the HLL Forum. This document is a prerelease (proposal) by Systerel to HLL Forum of an upcoming version 4.0.

  @techreport{bretonhal03356342,
      AUTHOR = "Breton, Nicolas",
      TITLE = "{High Level Language - Syntax and Semantics - Logical Foundation Document}",
      URL = "https://hal.science/hal-03356342",
      TYPE = "Technical Report",
      NUMBER = "C672 pr4.0 rc1 A",
      INSTITUTION = "{Systerel}",
      YEAR = "2021",
      MONTH = "September",
      KEYWORDS = "Formal Verification ; Modeling Language ; Model Checking ; HLL Forum ; HLL ; LFD",
      HAL_ID = "hal-03356342",
      HAL_VERSION = "v1"
  }
  

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▼]

  The Theory plug-in for the Rodin Platform enables modellers to extend the mathematical modelling notation for Event-B, with accompanying support for reasoning about the extended language. We consider in this presentation using Rodin theories to capture domain-specific Abstract Data Types (ADTs) and build dynamic systems using the developed structures. In particular, we proposed the notion of theory instantiation to incorporate more concrete representation of the ADTs. At the same time, the dynamic systems are refined further with respect to the changes of the underlying ADTs. We illustrate our approach with an industrial example of developing a train control system. We anticipate theory instantiation to be a promising direction for reusing theories via abstraction.

  @incollection{hoang2020domain,
      author = "Hoang, Thai Son and Voisin, Laurent and Butler, Michael",
      title = "Domain-Specific Developments Using Rodin Theories",
      booktitle = "Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems",
      pages = "19--37",
      year = "2020",
      publisher = "Springer",
      Abstract = "The Theory plug-in for the Rodin Platform enables modellers to extend the mathematical modelling notation for Event-B, with accompanying support for reasoning about the extended language. We consider in this presentation using Rodin theories to capture domain-specific Abstract Data Types (ADTs) and build dynamic systems using the developed structures. In particular, we proposed the notion of theory instantiation to incorporate more concrete representation of the ADTs. At the same time, the dynamic systems are refined further with respect to the changes of the underlying ADTs. We illustrate our approach with an industrial example of developing a train control system. We anticipate theory instantiation to be a promising direction for reusing theories via abstraction.",
      doi = "10.1007/978-981-15-5054-6\_2"
  }
  

• 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▼]

  The B-Method has an interesting history, where language and tools have evolved over the years. This not only led to considerable research and progress in the area of formal methods, but also to numerous industrial applications, in particular in the railway domain. We present a survey of the industrial usage of the B-Method since the first toolset in 1993 and the inauguration of the driverless metro line 14 in Paris in 1999. We discuss the various areas of applications, from software development to data validation and on to systems modelling. The evolution of the tooling landscape is also analysed, and we present an assessment of the current situation, lessons learned and possible new directions.

  @inproceedings{butler2020first,
      author = {Butler, Michael and K{\"o}rner, Philipp and Krings, Sebastian and Lecomte, Thierry and Leuschel, Michael and Mejia, Luis-Fernando and Voisin, Laurent},
      title = "The first twenty-five years of industrial use of the B-method",
      booktitle = "International Conference on Formal Methods for Industrial Critical Systems",
      pages = "189--209",
      year = "2020",
      organization = "Springer",
      Abstract = "The B-Method has an interesting history, where language and tools have evolved over the years. This not only led to considerable research and progress in the area of formal methods, but also to numerous industrial applications, in particular in the railway domain. We present a survey of the industrial usage of the B-Method since the first toolset in 1993 and the inauguration of the driverless metro line 14 in Paris in 1999. We discuss the various areas of applications, from software development to data validation and on to systems modelling. The evolution of the tooling landscape is also analysed, and we present an assessment of the current situation, lessons learned and possible new directions.",
      doi = "10.1007/978-3-030-58298-2\_8"
  }
  

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▼]

  Over the past decade, the growing number of safety-critical software in the railway signalling industry has led customers and industrials to look for efficient, cost-effective, verification and validation techniques. Formal methods, which have proven to be applicable and beneficial in terms of accuracy and completeness, are good candidates. However, they are still far from being used systematically for the verification of all safety-critical railway signalling systems. In order to evaluate their applicability, Alstom successfully experimented on its interlocking systems the model checking methods and tools developed by Systerel. This article describes the methodology used to industrialize this experimental model checking application process.

  @inproceedings{IFV,
      author = "Parillaud, Camille and Fonteneau, Yoann and Belmonte, Fabien",
      title = "Interlocking Formal Verification at Alstom Signalling",
      booktitle = "Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification - Third International Conference, RSSRail 2019, Lille, France, June 4-6, 2019, Proceedings",
      pages = "215--225",
      year = "2019",
      doi = "10.1007/978-3-030-18744-6\_14",
      timestamp = "Tue, 28 May 2019 13:30:19 +0200",
      biburl = "https://dblp.org/rec/bib/conf/rssrail/ParillaudFB19",
      bibsource = "dblp computer science bibliography, https://dblp.org"
  }
  

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▼]

  The goal of this communication is to analyze how to accommodate the constraints taken from two French standards. The first standard is the (CENELEC 61508, 2010) which aims at safe systems, while the second standard is the Common Criteria (ISO.IEC 15408, 2012), which aims at cyber-secure systems. The analysis focuses on the implementation of the OPC UA protocol (IEC 62541) in the development of S2OPC, which follows the research project INGOPCS. The analysis of the standards shows orthogonal philosophies between safety and cyber-security standards. The remainder of the communication details the different strategies that were applied to implement an OPC UA toolkit that respects both standards, with a focus on formal methods.

  @inproceedings{metayer2018vers,
      author = "Metayer, C and Humbert, P and Brameret, PA",
      title = "Vers une Implémentation S{\^u}re et Cybersécurisée du protocole OPC UA",
      booktitle = "Congrès Lambda Mu 21,« Ma{\^\i}trise des risques et transformation numérique: opportunités et menaces »",
      year = "2018"
  }
  

• 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▼]

  Event‐B is a formal notation and method for the systems development. The key feature of this method is to produce correct‐by‐construction system designs. Once the correct design is established, the remaining work is to generate or implement correct code from the design. Two main problems remain in the process from the correct‐by‐construction design to the correct software. First, the Event‐B design is “quasi‐correct” due to some technical limitations. For instance, it is still difficult to prove the liveness properties by the Rodin platform; it is not possible to construct the Event‐B design with floating‐point arithmetic, and sometimes, the Event‐B model is incomplete and must rely on the third‐party libraries. Therefore, a method is needed to complement these modeling and proof gaps. Secondly, proving the correctness of an automatic code generator is very difficult; therefore, a method is needed to guarantee the correctness of the produced code without proving the code generator. In this article, we address the above 2 problems by introducing an intermediate formal language called High‐Level Language (HLL) between the Event‐B models and the C code. The Event‐B model is translated to HLL with an additional schedule configuration, where Event‐B invariants and system invariants (here, deadlock‐freeness and liveness properties) are proved using a SAT‐based model checker called S3. This proof guarantees the correctness of the HLL model with respect to the Event‐B model. The C code is then automatically generated from the HLL model for most functions and is manually implemented for the third‐party ones according to the function contracts defined in Event‐B. The correctness of the generated C code is guaranteed using the equivalence proof, and the correctness of the implemented C code is guaranteed using the conformance proof. Through the article, we use a traffic light controller to illustrate the proposed method; then, we apply the method to an automatic protection function of a 3‐wheeled robot to evaluate its feasibility.

  @article{ge2018correct,
      author = "Ge, Ning and Dieumegard, Arnaud and Jenn, Eric and Voisin, Laurent",
      title = "Correct-by-construction specification to verified code",
      journal = "Journal of Software: Evolution and Process",
      volume = "30",
      number = "10",
      pages = "e1959",
      year = "2018",
      publisher = "Wiley Online Library"
  }
  

• 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▼]

  The software B method has so far been mainly used in the industrial world to develop safety critical software with very basic memory management limited to arrays of fixed size defined at compilation time.

  @inproceedings{badeau2018modelling,
      author = "Badeau, Frédéric and Lacroix, Vincent and Monfort, Vincent and Voisin, Laurent and Métayer, Christophe",
      title = "Modelling Dynamic Data Structures with the B Method",
      booktitle = "International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z",
      pages = "420--424",
      year = "2018",
      organization = "Springer"
  }
  

• 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▼]

  Although several authors like Zave and Jackson, Bjørner, Van Lamsweerde have drawn the attention of system designers on the necessity to handle domain knowledge, while designing systems, it is still a major concern nowadays.

  @inproceedings{AmeurACGHKMMSV18,
      author = "Ameur, Yamine Aït and Aït-Sadoune, Idir and Casteran, P. and Gibson, J. Paul and Hacid, Kahina and Kherroubi, Souad and M{\'{e}}ry, Dominique and Mohand-Oussaïd, Linda and Singh, Neeraj Kumar and Voisin, Laurent",
      title = "On the Importance of Explicit Domain Modelling in Refinement-Based Modelling Design. Experiments with Event-B",
      booktitle = "Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International Conference, {ABZ} 2018, Southampton, UK, June 5-8, 2018, Proceedings",
      pages = "425--430",
      year = "2018",
      crossref = "DBLP:conf/asm/2018",
      doi = "10.1007/978-3-319-91271-4\_35",
      timestamp = "Tue, 05 Jun 2018 13:06:59 +0200",
      biburl = "https://dblp.org/rec/bib/conf/asm/AmeurACGHKMMSV18",
      bibsource = "dblp computer science bibliography, https://dblp.org"
  }
  

• 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▼]

  Ce document RATP, basé sur un document original de Prover Technology, détaille la syntaxe ainsi que la sémantique du langage de modélisation formelle HLL (pour High Level Language). HLL est utilisé depuis plusieurs années à la RATP et par d’autres acteurs tels que SYSTEREL ou Prover Technology pour réaliser des vérifications formelles sur les logiciels critiques des CBTC et postes de signalisation.

  @techreport{ordioni:hal-01799749,
      AUTHOR = "Ordioni, Julien and Breton, Nicolas and Cola{\c c}o, Jean-Louis",
      TITLE = "{HLL v.2.7 Modelling Language Specification}",
      URL = "https://hal.archives-ouvertes.fr/hal-01799749",
      TYPE = "Other",
      NUMBER = "STF-16-01805",
      INSTITUTION = "{RATP}",
      YEAR = "2018",
      MONTH = "May",
      KEYWORDS = "Formal language ; HLL ; Specification ; SYSTEREL ; RATP ; Modelling language ; Prover technology",
      HAL_ID = "hal-01799749",
      HAL_VERSION = "v1"
  }
  

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▼]

  The Theory plug-in enables modellers to extend the mathematical modelling notation for Event-B, with accompanying support for reasoning about the extended language. Previous version of the Theory plug-in has been implemented based on Rodin 2.x. This presentation outline the main improvements to the The- ory plug-in, to be compatible with Rodin 3.x, in terms of both reliability and us- ability. We will also present the changes that were needed in the Rodin core to accommodate the Theory plug-in. Finally, we identify future enhancements and research directions for the Theory plug-in.

  @article{HoangVSBWB17,
      author = "Hoang, Thai Son and Voisin, Laurent and Salehi, A. and Butler, Michael J. and Wilkinson, Toby and Beauger, N.",
      title = "Theory Plug-in for Rodin 3.x",
      journal = "CoRR",
      volume = "abs/1701.08625",
      year = "2017",
      archivePrefix = "arXiv",
      eprint = "1701.08625",
      timestamp = "Wed, 07 Jun 2017 14:42:39 +0200",
      biburl = "https://dblp.org/rec/bib/journals/corr/HoangVSBWB17",
      bibsource = "dblp computer science bibliography, https://dblp.org"
  }
  

• 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▼]

  This paper presents a formal development process for safety-critical embedded Human-Machine Interface (HMI) systems. This formal approach is centered on the LIDL formal language and the S3 verification toolset. It is aimed at blurring the boundaries between modeling, design, verification and implementation for the development of HMI. From textual requirements to safety-critical embedded software, the development process integrates the following formal activities: modeling the behavioral aspect of user interfaces (UIs) using the LIDL language; translating LIDL to Lustre, with which we combine the functional library in Lustre; translating the Lustre design models into the HLL verification models; verifying formal properties expressed in HLL against the HLL model using the S3 toolset, and diagnosing design errors with the help of counterexample scenarios and debug tools. This formal development process is illustrated on a simple use case of part of the display component of an alert management system embedded in a three-wheeled robot.

  @inproceedings{ge:hal-01740640,
      AUTHOR = {Ge, Ning and Dieumegard, Arnaud and Jenn, Eric and d'Ausbourg, Bruno and A{\"i}t-Ameur, Yamine},
      TITLE = "{Formal development process of safety critical embedded human machine interface systems}",
      URL = "https://hal.archives-ouvertes.fr/hal-01740640",
      BOOKTITLE = "{TASE (11th International Symposium on Theoretical Aspects of Software Engineering)}",
      ADDRESS = "Sophia Antipolis, France",
      PAGES = "pp. 1-8",
      YEAR = "2017",
      MONTH = "September",
      tag = "s3,hll",
      KEYWORDS = "Safety-critical human machine interface system ; Formal methods ; Specification ; Verification ; LIDL ; Integration ; Lustre ; S3 ; HLL",
      HAL_ID = "hal-01740640",
      HAL_VERSION = "v1"
  }
  

• 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▼]

  The technical and academic aspects of the Event-B method , and the abstract description of its application in industrial contexts are the subjects of numerous publications. In this paper, we describe the experience of development engineers non familiar with Event-B to getting to grips with this method. We describe in details how we used the formalism, the refinement method, and its supporting toolset to develop the simple anti-collision function embedded in a small rolling robot. We show how the model has been developed from a set of high-level requirements and refined down to the software specification. For each phase of the development, we explain how we used the method, expose the encountered difficulties, and draw some practical lessons from this experiment.

  @inproceedings{dieumegard:hal-01535060,
      AUTHOR = "Dieumegard, Arnaud and Ge, Ning and Jenn, Eric",
      TITLE = "{Event-B at Work: Some Lessons Learnt from an Application to a Robot Anti-collision Function}",
      URL = "https://hal.archives-ouvertes.fr/hal-01535060",
      BOOKTITLE = "{9th International Symposium on NASA Formal Methods (NFM 2017)}",
      ADDRESS = "Moffet Field, CA, United States",
      SERIES = "NASA Formal Methods 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings",
      VOLUME = "10227",
      PAGES = "312-341",
      YEAR = "2017",
      tag = "eventb, b",
      MONTH = "May",
      DOI = "10.1007/978-3-319-57288-8\\_24",
      KEYWORDS = "Formal refinement ; software verification ; formal verifiication ; anti-collision ; Event-B",
      HAL_ID = "hal-01535060",
      HAL_VERSION = "v1"
  }
  

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▼]

  Model checking has made a lot of progress since its infancy. For a long time, industrial applications were still limited to some very specific domains out of which the technique bumps into the state explosion wall. Nowadays things evolve and some tools are able to tackle real world use cases outside of the known domains. We give here the feedback collected when using model checking on several industrial strength use cases and give indication on how we take into account the specific domain constraints. 1 Model Checking for Industrial Problems Model checking refers to the problem of exhaustively and automatically checking whether a given model of a system meets a given specification. Model Checking is now an old technique which takes its ground in the mid 1970s as a response to concurrent problem analysis. It was until recently essentially confined to some specific areas, such as hardware analysis or protocol verification. Extension to other domains such as software verification has always been difficult due to the combinatorial explosion problem (the size of the space state grows exponentially with the size of the problem to analyze). However, recent developments in a variety of fields, ranging from symbolic model checking to SAT solver engines and including model checker parallelization lead to a broader range of application in industry including software analysis.

  @inproceedings{clabaut-hal-01291365,
      AUTHOR = "Clabaut, Mathieu and Ge, Ning and BRETON, Nicolas and Jenn, Eric and Delmas, Rémi and Fonteneau, Yoann",
      TITLE = "{Industrial Grade Model Checking Use Cases, Constraints, Tools and Applications}",
      URL = "https://hal.archives-ouvertes.fr/hal-01291365",
      BOOKTITLE = "{8th European Congress on Embedded Real Time Software and Systems (ERTS 2016)}",
      ADDRESS = "TOULOUSE, France",
      YEAR = "2016",
      MONTH = "January",
      KEYWORDS = "model checking ; safety proof ; equivalence checking ; constraint solving ; test case generation ; EN 50128 ; DO 178C ; industrial size model ; formal method"
  }
  

• Ning Ge, Arnaud Dieumegard, Eric Jenn, and Laurent Voisin. From event-b to verified c via hll. CoRR, 2016. arXiv:1610.07410.
  [abstract▼] [BibTeX▼]

  This work addresses the correct translation of an Event-B model to C code via an intermediate formal language, HLL. The proof of correctness follows two main steps. First, the final refinement of the Event-B model, including invariants, is translated to HLL. At that point, additional properties (e.g., deadlock-freeness, liveness properties, etc.) are added to the HLL model. The proof of the invariants and additional properties at the HLL level guarantees the correctness of the translation. Second, the C code is automatically generated from the HLL model for most of the system functions and manually for the remaining ones; in this case, the HLL model provides formal contracts to the software developer. An equivalence proof between the C code and the HLL model guarantees the correctness of the code.

  @article{ge2016event,
      author = "Ge, Ning and Dieumegard, Arnaud and Jenn, Eric and Voisin, Laurent",
      title = "From Event-B to verified C via HLL",
      journal = "CoRR",
      volume = "abs/1610.07410",
      eprint = "1610.07410",
      biburl = "https://dblp.org/rec/bib/journals/corr/GeDJV16",
      year = "2016"
  }
  

• 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▼]

  In this paper, we integrate inductive proof, bounded model checking, test case generation and equivalence proof techniques to verify an embedded system. This approach is implemented using the Systerel Smart Solver (S3) toolset. It is applied to verify properties at system, software, and code levels. The verification process is illustrated on an anti-collision system (ARP for Automatic Rover Protection) implemented on-board a rover. Focus is placed on the verification of safety and functional properties and the proof of equivalence between the design model and the generated code.

  @inproceedings{GeJBF16,
      author = "Ge, Ning and Jenn, Eric and Breton, Nicolas and Fonteneau, Yoann",
      title = "Formal Verification of a Rover Anti-collision System",
      booktitle = "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",
      pages = "171--188",
      year = "2016",
      crossref = "DBLP:conf/fmics/2016",
      doi = "10.1007/978-3-319-45943-1\_12",
      timestamp = "Sun, 21 May 2017 00:22:12 +0200",
      biburl = "https://dblp.org/rec/bib/conf/fmics/GeJBF16",
      bibsource = "dblp computer science bibliography, https://dblp.org"
  }
  

• 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▼]

  Systerel Smart Solver (S3) is a formal verification toolset built around a synchronous modeling language (HLL), and a SAT-based symbolic Model Checker developed by Systerel. It allows building efficient formal verification solutions specially fitted for a given mission in a given development process, with a built-in focus on trustworthiness. The architecture of such a solution is described, and its application to the proof of high-level properties unambiguously implying the safety of large industrial railway control systems is reported.

  @inproceedings{BretonF16,
      author = "Breton, Nicolas and Fonteneau, Yoann",
      title = "{S3:} Proving the Safety of Critical Systems",
      booktitle = "Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification - First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings",
      pages = "231--242",
      year = "2016",
      crossref = "DBLP:conf/rssrail/2016",
      doi = "10.1007/978-3-319-33951-1\_17",
      timestamp = "Thu, 22 Feb 2018 18:20:59 +0100",
      biburl = "https://dblp.org/rec/bib/conf/rssrail/BretonF16",
      bibsource = "dblp computer science bibliography, https://dblp.org"
  }
  

• 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▼]

  In railway control systems, distributed, available and reliable software is a recurrent need. As a consequence a middleware is a convenient solution to handle these aspects and provide guarantees to the application soft-ware. In this context, we developed a new Ada 2012 middleware for execution of distributed and hot-redundant software which must conform with EN50128 standard.This article presents the particular needs of such a middleware, the technical challenges and solutions, and a feedback on the Ada 2012 language and tools

  @article{monfort2016middleware,
      author = "Monfort, Vincent",
      title = "Middleware for a Distributed and Hot-redundant Software in Ada 2012",
      journal = "ADA USER",
      volume = "37",
      number = "4",
      pages = "207",
      year = "2016",
      url = "https://www.systerel.fr/wp-content/uploads/2017/01/AUJ\_middleware\_A\_published.pdf",
      Abstract = "In railway control systems, distributed, available and reliable software is a recurrent need. As a consequence a middleware is a convenient solution to handle these aspects and provide guarantees to the application soft-ware. In this context, we developed a new Ada 2012 middleware for execution of distributed and hot-redundant software which must conform with EN50128 standard.This article presents the particular needs of such a middleware, the technical challenges and solutions, and a feedback on the Ada 2012 language and tools"
  }
  

• 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▼]

  This paper gives an overview of small-tALCQe, an experi-mental programming environment for a graph transformation languagethat is based on the ALCQ description logic. small-tALCQe not onlyallows developers coding and executing graph transformations but alsoassists them in analyzing and verifying their codes. We describe the com-ponents that make up small-tALCQe: the transformation language itself,the compiler for generating executable transformations, the code ana-lyzers and the prover for reasoning about transformations. All of theminteract under the hood of an Eclipse user interface to provide differentlevels of assistance for achieving correct graph transformations.

  @inproceedings{hal-02879713,
      AUTHOR = {Baklanova, Nadezhda and Brenas, Jon Ha{\"e}l and Makhlouf, Amani and Percebois, Christian and Strecker, Martin and Tran, Hanh Nhi},
      TITLE = "{Coding, Executing and Verifying Graph Transformations with small-tALCQe}",
      URL = "https://hal.archives-ouvertes.fr/hal-02879713",
      BOOKTITLE = "{International Workshop Graph Computation Models, Part of STAF 2016 (GCM 2016)}",
      ADDRESS = "Vienna, Austria",
      PAGES = "1-15",
      YEAR = "2016",
      MONTH = "July",
      KEYWORDS = "Software analysis ; Graph transformations ; Program testing ; Counterexample generation ; Program verification",
      HAL_ID = "hal-02879713",
      HAL_VERSION = "v1",
      Abstract = "This paper gives an overview of small-tALCQe, an experi-mental programming environment for a graph transformation languagethat is based on the ALCQ description logic. small-tALCQe not onlyallows developers coding and executing graph transformations but alsoassists them in analyzing and verifying their codes. We describe the com-ponents that make up small-tALCQe: the transformation language itself,the compiler for generating executable transformations, the code ana-lyzers and the prover for reasoning about transformations. All of theminteract under the hood of an Eclipse user interface to provide differentlevels of assistance for achieving correct graph transformations."
  }
  

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▼]

  In this paper, the challenges for using formal verification based on automatic tools, like model-checkers, in the industrial development process of safety critical systems is discussed. This usage must be integrated into an appropriate process and must allow for independent result-checking. Our approach is illustrated with a case study from the openETCS ITEA2 research project using the Systerel Smart Solver S3, a modern SAT-based model-checker for equivalence checking and safety properties analysis of SCADE, C or Ada programs.

  @inproceedings{Petit-DocheBCFG15,
      author = {Petit{-}Doche, Marielle and Breton, Nicolas and Courbis, Rom{\'{e}}o and Fonteneau, Yoann and G{\"{u}}demann, Matthias},
      title = "Formal Verification of Industrial Critical Software",
      booktitle = "Formal Methods for Industrial Critical Systems - 20th International Workshop, {FMICS} 2015, Oslo, Norway, June 22-23, 2015 Proceedings",
      pages = "1--11",
      year = "2015",
      crossref = "DBLP:conf/fmics/2015",
      doi = "10.1007/978-3-319-19458-5\_1",
      timestamp = "Fri, 25 Aug 2017 06:45:03 +0200",
      biburl = "https://dblp.org/rec/bib/conf/fmics/Petit-DocheBCFG15",
      bibsource = "dblp computer science bibliography, https://dblp.org"
  }
  

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▼]

  This paper describes the process of data validation for railway safety-critical computer-based systems formally implemented by Systerel as supplier of railway industry’s companies. More precisely, it describes the validation of data against the requirements it has to meet to ensure systems safety. International standards, especially CENELEC EN 50128, recommend the use of formal methods for designing the most critical safety-related systems. We use the OVADO formal tool to perform data validation. For that, we model data requirements by using the specification language of the B method, namely the B language, before using OVADO that automatically checks that data meet requirements. This tool integrates two independent components that must give the same results when they are applied on the same data, according to the principle of redundancy. An example of data validation for a CBTC system is also given.

  @inbook{ovado,
      author = "Abo, Robert and Voisin, Laurent and Counsell, Steve and N{\'u}{\\textasciitilde {n}}ez, Manuel",
      title = "Formal Implementation of Data Validation for Railway Safety-Related Systems with OVADO",
      bookTitle = "Software Engineering and Formal Methods: SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD, and OpenCert, Madrid, Spain, September 23-24, 2013, Revised Selected Papers",
      year = "2014",
      publisher = "Springer International Publishing",
      address = "Cham",
      pages = "221--236",
      isbn = "978-3-319-05032-4",
      doi = "10.1007/978-3-319-05032-4\_17"
  }
  

• 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▼]

  Systerel is an SME specializing in the development of safety‐critical real‐time systems. The question of data verification is related to efforts to reduce the development costs of safe, software‐based complex systems. This chapter describes the requirements and solutions associated with the verification of configuration data. The classic system specification and design cycle using subsystems, subsequently refined into material and software components, potentially over the course of multiple iterations, involves a number of functional and non‐functional requirements. Once data with known properties has been produced, the next stage is to verify the conformity of the data with the identified properties. The chapter describes the different methods used for this purpose. It provides a significant contribution to improving the quality of verifications of the associated process.

  @article{clabaut2014formal,
      author = "Clabaut, Mathieu",
      title = "Formal Verification of Data for Parameterized Systems",
      journal = "Formal Methods Applied to Industrial Complex Systems",
      doi = "10.1002/9781119004707.ch5",
      pages = "115--135",
      year = "2014",
      publisher = "Wiley Online Library"
  }
  

• 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▼]

  The aim of this chapter is to show that practices widely used in classic developments can also be applied in the context of formal processes, facilitating their implementation and acceptability. In the context of modern industry, it is rare to find development projects for systems, equipment or software which do not include the creation of one or more prototypes in the earliest stages. The chapter provides some elements of response to these issues concerning the relationships and responsibilities of the development and validation teams. B is known and used in relation to safety requirements. The B method for software can be used to improve practices based on event‐B, and vice‐versa. The use of formal methods such as B allows engineers to focus on their primary role in specifying and designing systems or programs, using powerful reasoning tools, without needing to devote time and effort to later, purely coding‐related stages.

  @article{metayer2014pragmatic,
      author = "Metayer, Christophe and Bustany, Fran{\c{c}}ois and Clabaut, Mathieu",
      title = "Pragmatic Use of B: The Power of Formal Methods without the Bulk",
      journal = "Formal Methods Applied to Complex Systems: Implementation of the B Method",
      pages = "187--200",
      year = "2014",
      publisher = "Wiley Online Library",
      doi = "10.1002/9781119002727.ch7"
  }
  

• 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▼]

  In this talk, we give an historical account of the development of the Rodin Platform during the last 10 years.

  @inproceedings{VoisinA14,
      author = "Voisin, Laurent and Abrial, Jean{-}Raymond",
      title = "The Rodin Platform Has Turned Ten",
      booktitle = "Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings",
      pages = "1--8",
      year = "2014",
      crossref = "DBLP:conf/asm/2014",
      doi = "10.1007/978-3-662-43652-3\_1",
      timestamp = "Sun, 21 May 2017 00:18:58 +0200",
      biburl = "https://dblp.org/rec/bib/conf/asm/VoisinA14",
      bibsource = "dblp computer science bibliography, https://dblp.org"
  }
  

• 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▼]

  Formal development in Event-B generally requires the validation of a large number of proof obligations. Some tools automatically discharge a significant part of them, thus augmenting the efficiency of the formal development. We here investigate the use of SMT (Satisfiability Modulo Theories) solvers in addition to the traditional tools, and detail the techniques used for the cooperation between the Rodin platform and SMT solvers. Our contribution is the definition of a translation of Event-B proof obligations to the language of SMT solvers, its implementation in a Rodin plug-in, and an experimental evaluation on a large sample of industrial and academic projects. On this domain, adding SMT solvers to Atelier B provers reduces significantly the number of sequents that need to be proved interactively.

  @article{rodinSMT,
      author = "Déharbe, David and Fontaine, Pascal and Guyot, Yoann and Voisin, Laurent",
      title = "Integrating {SMT} Solvers in {R}odin",
      journal = "scp",
      volume = "94",
      number = "P2",
      year = "2014",
      pages = "130--143",
      publisher = "Elsevier",
      doi = "10.1016/j.scico.2014.04.012"
  }
  

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▼]

  Formal development in Event-B generally requires the validation of a large number of proof obligations. Some automatic tools exist to automatically discharge a significant part of them, thus augmenting the efficiency of the formal development. We here investigate the use of SMT (Satisfiability Modulo Theories) solvers in addition to the traditional tools, and detail the techniques used for the cooperation between the Rodin platform and SMT solvers. Our contribution is the definition of two approaches to use SMT solvers, their implementation in a Rodin plug-in, and an experimental evaluation on a large sample of industrial and academic projects. Adding SMT solvers to Atelier B provers reduces to one fourth the number of sequents that need to be proved interactively.

  @inproceedings{deharbe2012smt,
      author = "Déharbe, David and Fontaine, Pascal and Guyot, Yoann and Voisin, Laurent",
      title = "SMT solvers for Rodin",
      booktitle = "International Conference on Abstract State Machines, Alloy, B, VDM, and Z",
      pages = "194--207",
      year = "2012",
      organization = "Springer"
  }
  

• Frédéric Badeau and Marielle Doche-Petit. Formal data validation with event-b. CoRR, 2012. arXiv:1210.7039.
  [abstract▼] [BibTeX▼]

  This article presents a verification and validation activity performed in an industrial context, to validate configuration data of a metro CBTC system by creating a formal B model of these configuration data and of their properties. A double tool chain is used to safely check whether a certain given input of configuration data fulfill its properties. One tool is based on some Rodin and open source plug-ins and the other tool is based on ProB.

  @article{badeau2012formal,
      author = "Badeau, Frédéric and Doche-Petit, Marielle",
      title = "Formal data validation with Event-B",
      journal = "CoRR",
      volume = "abs/1210.7039",
      eprint = "1210.7039",
      biburl = "https://dblp.org/rec/bib/journals/corr/abs-1210-7039",
      year = "2012"
  }
  

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▼]

  Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. In this article we present the Rodin modelling tool that seamlessly integrates modelling and proving. We outline how the Event-B language was designed to facilitate proof and how the tool has been designed to support changes to models while minimising the impact of changes on existing proofs. We outline the important features of the prover architecture and explain how well-definedness is treated. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.

  @article{rodin,
      author = "Abrial, Jean-Raymond and Butler, Michael and Hallerstede, Stefan and Hoang, Thai Son and Mehta, Farhad and Voisin, Laurent",
      title = "Rodin: an open toolset for modelling and reasoning in Event-B",
      journal = "International Journal on Software Tools for Technology Transfer",
      year = "2010",
      volume = "12",
      number = "6",
      pages = "447--466",
      issn = "1433-2787",
      doi = "10.1007/s10009-010-0145-y"
  }
  

• 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▼]

  Nowadays lot of critical systems used in aeronautic, aerospace, automotive and railway domains are designed to be highly configurable. In such systems, the data configuration validity is of tremendous importance.The railway domain does already apply some formal techniques to validate configuration data. This study, funded by the CNES, demonstrates the suitability of such methods for validation of flight software configuration data.

  @article{clabaut20104b,
      author = "Clabaut, Mathieu and Metayer, Christophe and Morand, Eric",
      title = "Formal Data Validation — formal techniques applied to verification of data properties",
      journal = "Embedded Real Time Software and Systems ERTS",
      year = "2010"
  }
  

2009¶

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

  @misc{abrial2009rodin,
      author = "Abrial, Jean-Raymond and Metayer, Christophe and Voisin, Laurent",
      title = "Rodin manual and language definition",
      year = "2009",
      publisher = "RODIN Project"
  }
  

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▼]

  Some RATP units are responsible for evolution and maintenance of an automated interlocking specification document. In order to improve their paper and pencil process, RATP asked Systerel if Event-B could be useful to them. An eight month study was launched whose main goal was to help RATP improving their confidence in their interlocking specification, by applying an Event-B approach on rewriting their requirement document.

  @inproceedings{metayer2008dir,
      author = "Metayer, Christophe and Clabaut, Mathieu",
      title = "DIR 41 Case Study",
      booktitle = "International Conference on Abstract State Machines, B and Z",
      pages = "357--357",
      year = "2008",
      organization = "Springer",
      doi = "10.1007/978-3-540-87603-8\_44"
  }
  

• 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▼]

  @inproceedings{soton266769,
      author = "Abrial, Jean-Raymond and Butler, Michael and Hallerstede, Stefan and Voisin, Laurent",
      booktitle = "Abstract State Machines, B and Z, First International Conference ABZ 2008",
      month = "September",
      title = "A Roadmap for the Rodin Toolset",
      year = "2008",
      pages = "347",
      url = "https://eprints.soton.ac.uk/266769/"
  }
  

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▼]

  Firewall administration is not a task free from pitfalls. Some interfaces exist to alleviate the administrator burden, but none is formally proven, and none is generic enough to manage appliances from different vendors. A study was lead to develop such a formal interface.

  @inproceedings{clabaut2007tool,
      author = "Clabaut, Mathieu",
      title = "A Tool for Firewall Administration",
      booktitle = "B 2007: Formal Specification and Development in B, 7th International Conference of {B} Users, Besan{\c{c}}on, France, January 17-19, 2007, Proceedings",
      pages = "255--256",
      year = "2007",
      crossref = "DBLP:conf/b/2007",
      doi = "10.1007/11955757\_22",
      timestamp = "Tue, 14 May 2019 10:00:35 +0200",
      biburl = "https://dblp.org/rec/bib/conf/b/Clabaut07",
      bibsource = "dblp computer science bibliography, https://dblp.org"
  }
  

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▼]

  @inproceedings{AbrialBHV06,
      author = "Abrial, Jean-Raymond and Butler, Michael and Hallerstede, Stefan and Voisin, Laurent",
      title = "An Open Extensible Tool Environment for {Event-B}",
      booktitle = "ICFEM",
      year = "2006",
      pages = "588-605",
      bibsource = "DBLP, http://dblp.uni-trier.de",
      ee = "http://dx.doi.org/10.1007/11901433\_32",
      owner = "Ali Gondal",
      timestamp = "2008.05.28"
  }
  

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▼]

  In this article we would like to go back on B used to design software, by presenting the industrial process established through years by Siemens Transportation Systems on a real project: the VAL shuttle for Roissy Charles de Gaulle airport. In this project, the logical core of an equipment located along the tracks and driving the shuttles is designed with B. By confronting this B software development, with the historical context, we show that B can be used as a high-level programming language offering the feature of proving properties. We show how this process is used to build, by construction, a large size software with very few design errors ever since its first release, and for a predefined cost.

  @inproceedings{Roissy,
      author = "Badeau, Fr{\'{e}}d{\'{e}}ric and Amelot, Arnaud",
      title = "Using {B} as a High Level Programming Language in an Industrial Project: Roissy {VAL}",
      booktitle = "{ZB} 2005",
      pages = "334--354",
      year = "2005",
      crossref = "DBLP:conf/zum/2005",
      doi = "10.1007/11415787\_20",
      timestamp = "Tue, 30 May 2017 16:36:52 +0200",
      biburl = "http://dblp.org/rec/bib/conf/zum/BadeauA05",
      bibsource = "dblp computer science bibliography, http://dblp.org"
  }
  

• 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▼]

  @techreport{MAV:05,
      author = "Métayer, C. and Abrial, J.-R. and Voisin, L.",
      title = "Event-{B} {L}anguage",
      institution = "EU Project IST-511599 - RODIN",
      year = "2005",
      number = "Deliverable 3.2",
      month = "May",
      note = "http://rodin.cs.ncl.ac.uk"
  }
  

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▼]

  Cet article présente quelques résultats du projet RNTL BOM (B Optimisant la Mémoire). Le but était d’obtenir un traducteur du langage B vers le langage C, facilement adaptable à des contraintes mémoire (logiciels embarqués sur cartes à puce). Nous proposons une méthode d’extension des types de base permettant d’inclure certains types du langage cible. Nous présentons comment le traducteur est décrit sous forme de règles de traduction pour permettre d’adapter la traduction aux plate-formes cibles. Nous indiquons une démarche pour assurer la correction du code produit. Nous terminons par quelques mesures de taille de code généré pour la machine virtuelle Java Card.

  @article{BadeauBBMPSV04,
      Author = "Badeau, Frédéric and Bert, Didier and Boulmé, Sylvain and Métayer, Christophe and Potet, Marie-Laure and Stouls, Nicolas and Voisin, Laurent",
      Bibsource = "DBLP, http://dblp.uni-trier.de",
      Date-Added = "2014-01-24 23:40:16 +0000",
      Date-Modified = "2014-01-24 23:41:18 +0000",
      doi = "10.3166/tsi.23.879-903",
      Journal = "Technique et Science Informatiques",
      Number = "7",
      Pages = "879-903",
      Read = "1",
      Title = "Adaptabilité et validation de la traduction de B vers C. Points de vue et résultats du projet BOM",
      Volume = "23",
      Year = "2004",
      Abstract = "Cet article présente quelques résultats du projet RNTL BOM (B Optimisant la Mémoire). Le but était d'obtenir un traducteur du langage B vers le langage C, facilement adaptable à des contraintes mémoire (logiciels embarqués sur cartes à puce). Nous proposons une méthode d'extension des types de base permettant d'inclure certains types du langage cible. Nous présentons comment le traducteur est décrit sous forme de règles de traduction pour permettre d'adapter la traduction aux plate-formes cibles. Nous indiquons une démarche pour assurer la correction du code produit. Nous terminons par quelques mesures de taille de code généré pour la machine virtuelle Java Card."
  }
  

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▼]

  This paper presents the results of the RNTL BOM project, which aimed to develop an approach to generate efficient code from B formal developments. The target domain is smart card applications, in which memory and code size is an important factor. The results detailed in this paper are a new architecture of the translation process, a way to adapt the B0 language in order to include types of the target language and a set of validated optimizations. An assessment of the proposed approach is given through a case study, relative to the development of a Java Card Virtual Machine environment.

  @inproceedings{BertBPRV03,
      Author = "Bert, Didier and Boulmé, Sylvain and Potet, Marie-Laure and Requet, Antoine and Voisin, Laurent",
      Bibsource = "DBLP, http://dblp.uni-trier.de",
      Booktitle = "FME",
      Crossref = "DBLP:conf/fm/2003",
      Date-Added = "2014-01-24 23:41:54 +0000",
      Date-Modified = "2014-01-24 23:42:37 +0000",
      doi = "10.1007/978-3-540-45236-2\_7",
      Pages = "94-113",
      Read = "1",
      Title = "Adaptable Translator of B Specifications to Embedded C Programs",
      Year = "2003",
      Abstract = "This paper presents the results of the RNTL BOM project, which aimed to develop an approach to generate efficient code from B formal developments. The target domain is smart card applications, in which memory and code size is an important factor. The results detailed in this paper are a new architecture of the translation process, a way to adapt the B0 language in order to include types of the target language and a set of validated optimizations. An assessment of the proposed approach is given through a case study, relative to the development of a Java Card Virtual Machine environment."
  }