Bibliography

August 2024
Formal Aspects of Computing

Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

October 2024
Conference DISCoRail 2024, Heraklion

ERTMS aims to facilitate train traffic in Europe by providing a single, interoperable framework. ERTMS represents a set of several thousand pages of specification, covering both high-level and (very) lowlevel aspects. Since its creation in the 1990s, it has evolved regularly, with baseline 4 being published in 2023. However, it is proving rather difficult to implement and deploy. It has little feedback compared with the history of the railway world in general, particularly for the highest levels of supervision. The specification, expressed in the form of thematic SUBSETS, give direction but leave a great deal of freedom to manufacturers.
The verification work being carried out today relates to the compliance of on-board and trackside equipment with the SUBSETS of the standard, mainly by means of simulation and test benches. This article presents
some of the formal verification and validation methods, including formal modelling, automatic proof and model-checking, that are being used today to improve the confidence level of actual deployments.

September 2024
Conference FM 2024, Milan, keynote

Software development for mission-critical applications requires a level of confidence that can be achieved through the use of formal methods. For a number of industrial applications, there is a lack of high-level properties to be verified, and proof mainly replaces unit testing.
This presentation explores an integrated approach based on more than 20 years of industrial practice, which enables so-called “system” properties to be modelled in a formal software model. The proof of the system’s safety is not carried out entirely formally, but it is entirely guided by the model. It is based on 2 principles which are illustrated by means of a demonstrative example.

March 2024
Conference: Mathematical Proof and Software Safety. Fondation Sciences Mathématiques de Paris. Paris
Thierry Lecomte

CLEARSY puts societal issues, regulatory needs and technical challenges into perspective in order to explain how and why the reasoned use of formal methods makes it possible to better control the safety of critical systems, which are essential to our society. The presentation refers to the formal modelling and proof of software and its parameters, as well as to the engineering of safety reasoning.

October 2022
DOI: 10.1007/978-3-031-19762-8_22
In book: Leveraging Applications of Formal Methods, Verification and Validation.
Jan Peleska, Anne Haxthausen, Thierry Lecomte

In this paper, we review software-based technologies already known to be, or expected to become essential for autonomous train control systems with grade of automation GoA 4 (unattended train operation) in existing open railway environments. It is discussed which types of technology can be developed and certified already today on the basis of existing railway standards. Other essential technologies, however, require modifications or extensions of existing standards, in order to provide a certification basis for introducing these technologies into non-experimental “real-world” rail operation. Regarding these, we check the novel pre-standard ANSI/UL 4600 with respect to suitability as a certification basis for safety-critical autonomous train control functions based on methods from artificial intelligence. As a thought experiment, we propose a novel autonomous train controller design and perform an evaluation according to ANSI/UL 4600. This results in the insight that autonomous freight trains and metro trains using this design could be evaluated and certified on the basis of ANSI/UL 4600 .

January 2022
DOI: 10.1007/978-3-031-05814-1_9
In book: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
Lilian Burdy, David Déharbe, Denis Sabatier

The B method is a formal method to design software components and to prove that they are compliant with some formalized requirements, giving a way to build safety-critical programs. However, the correctness of the obtained programs obviously rely on the correctness of those formalized software requirements. Using the CLEARSY Safety Platform, a vital processing solution developed by CLEARSY (SIL4 certified, Certifer 9594/0262) with native B capabilities, we demonstrate here a method to develop vital software with formal proofs directly attached to the key system properties. For instance, a train localization system is proven regarding the property stating that the computed location interval shall always contain the actual train. Such proofs become possible by combining software variables with variables representing physical entities and their timed evolution, thanks to the guaranteed time and deadlines of the CLEARSY Safety Platform. Thus, we avoid the problem of ensuring the correctness of a complex set of formalized software requirements by directly ensuring the wanted system properties. Assumptions and properties for the non-software parts are included in the same B model used to develop the software on the CLEARSY Safety Platform.

May 2022
DOI: 10.1007/978-3-031-05760-1_29
Conference: Research Challenges in Information Science: Ethics and Trustworthiness in Information Science (RCIS 2022). To appear.At: Barcelona, SpainVolume: LNBIP 446, Springer
Akram Idani

Existing surveys about language workbenches (LWBs) ranging from 2006 to 2019 observe a poor usage of formal methods within domain-specific languages (DSLs) and call for identifying the reasons. We believe that the lack of automated formal reasoning in LWBs, and more generally in MDE, is not due to the complexity of formal methods and their mathematical background, but originates from the lack of initiatives that are dedicated to the integration of existing tools and techniques. To this aim we developed the Meeduse LWB and investigated the use of the B method to rigorously define the semantics of DSLs. The current applications of Meeduse show that the integration of DSLs together with theorem proving, animation and model-checking is viable and should be explored further. This technique is especially interesting for executable DSLs (xDSLs), which are DSLs with behavioural features. This paper is a review of our Formal MDE (FMDE) approach for xDSLs and a proposal for new avenues of investigation.

February 2023
DOI: 10.1007/978-3-031-26236-4_12
Conference: Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops. SEFM 2022. At: Berlin, Germany. Volume: LNCS 13765, Springer
Léa Riant

Insightful error reports save precious time in the design of systems. When using the formal B method, design errors correspond to invalid proof obligations. The legacy automatic provers in Atelier B are not capable to identify if a failure to prove is due to a logical error. In contrast, SMT solvers are capable to prove a first-order logic formula but also to disprove it and to produce a counter-example. Those counter-examples can give precious indications to the user on design errors. SMT solvers have been integrated in the most recent version of Atelier B, but only to use their proving capabilities. We present here counter_example_reader, a tool to interpret a counter-example produced by an SMT solver into a B counter-example.

August 2020
DOI: 10.1007/978-3-030-58298-2_8
In book: Formal Methods for Industrial Critical Systems
Michael Butler, Philipp Körner, Sebastian Krings, Laurent Voisin, Thierry Lecomte, Fernando Mejia, Michael Leuschel

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.

May 2020
DOI: 10.1007/978-3-030-48077-6_20
In book: Rigorous State-Based Methods
Héctor Ruíz Barradas, Lilian Burdy, David Déharbe

Proof obligations of the B method and of Event B use predicates in the Constraints, Sets, Properties and Invariant clauses as hypotheses in proof obligations. A contradiction in these predicates results in trivially valid proof obligations and essentially voids the development. A textbook on the B method [3] presents three “existence proof obligations” to show the satisfiability of the Constraints, Properties and Invariant clauses as soon as they are stated in a component. Together with new existence proof obligations for refinement, this prevents the introduction of such contradictions in the refinement chain. This paper presents a detailed formalization of these existence proof obligations, specifying their implementation in Atelier B.

May 2020
LicenseCC BY 4.0
Project: LCHIP: Low Cost, High Integrity Platform
Thierry Lecomte, David Déharbe, Denis Sabatier, Sylvain Conchon

Developing safety critical applications often require rare human resources to complete successfully while off-the-shelf block solutions appear difficult to adapt especially during short-term projects. The CLEARSY Safety Platform fulfils a need for a technical solution to overcome the difficulties to develop SIL3/SIL4 system with its technology based on a double-processor and a formal method with proof to ensure safety at the highest level. The formal method, namely the B method, has been heavily used in the railways industry for decades. Using its IDE, Atelier B, to program the CLEARSY Safety Platform ensures a higherlevel of confidence on the software generated. This paper presents this platform aimed at revolutionising the development of safety critical systems, developed through the FUI project LCHIP (Low Cost High Integrity Platform).

August 2020
DOI: 10.1007/978-3-030-58298-2_9
In book: Formal Methods for Industrial Critical Systems
Thierry Lecomte, Bruno Lavaud, Denis Sabatier, Lilian Burdy

The CLEARSY Safety Platform (CSSP) is both a hardware and software platform aimed at developing safety critical applications. A smart combination of hardware features (double processor) and formal method (B method and code generators) was used to produce a SIL4-ready platform where safety principles are built-in. A first version, SK0, was released for education purpose with a restricted application template. An industry-strength version, CS0, was then released, providing more degrees of freedom at the cost of a more tricky development and engineering process. This article presents the new CS0 modelling paradigm, lists the conditions to be verified by the system developed, and briefly introduces a first application, software only: a safety flasher.

August 2020
DOI: 10.1007/978-3-030-54994-7_2
In book: Formal Methods. FM 2019 International Workshops
Thierry Lecomte

Industrial applications involving formal methods are still exceptions to the general rule. Lack of understanding, employees without proper education, difficulty to integrate existing development cycles, no explicit requirement from the market, etc. are explanations often heard for not being more formal. This article reports some experience about a game changer that is going to seamlessly integrate formal methods into safety critical systems engineering.

May 2020
DOI: 10.1007/978-3-030-48077-6_9
In book: Rigorous State-Based Methods
Project: LCHIP: Low Cost, High Integrity Platform
Thierry Lecomte

The CLEARSY Safety Platform (CSSP) is aimed at easing the development and the deployment of safety critical applications, up to the safety integrity level 4 (SIL4). It relies on the smart integration of the B formal method, redundant code generation and compilation, and a hardware platform that ensures a safe execution of the software. This paper exposes the programming model of the CSSP used to develop control & command applications based on digital I/Os.

December 2020Innovations in Systems and Software Engineering 16(C)
DOI: 10.1007/s11334-020-00366-3
Akram Idani, Yves Ledru, Germán Vega

Model-driven engineering (MDE) promotes the use of models throughout the software development cycle in order to increase abstraction and reduce software complexity. It favors the definition of domain-specific modeling languages (DSMLs) thanks to frameworks dedicated to meta-modeling and code generation like EMF (Eclipse Modeling Framework). The standard semantics of meta-models allows interoperability between tools such as language analysers (e.g., XText), code generators (e.g., Acceleo), and also model transformation tools (e.g., ATL). However, a major limitation of MDE is the lack of formal reasoning tools allowing to ensure the correctness of models. Indeed, most of the verification activities offered by MDE tools are based on the verification of OCL constraints on instances of meta-models. However, these constraints mainly deal with structural properties of the model and often miss out its behavioral semantics. In this work, we propose to bridge the gap between MDE and the rigorous world of formal methods in order to guarantee the correctness of both structural and behavioral properties of the model. Our approach translates EMF meta-models into an equivalent formal B specification and then injects models into this specification. The equivalence between the resulting B specification and the original EMF model is kept by proven design steps leading to a rigorous MDE technique. The AtelierB prover is used to guarantee the correctness of the model’s behavior with respect to its invariant properties, and the ProB model-checker is used to animate underlying execution scenarios which are translated back to the initial EMF model. Besides the use of these automatic reasoning tools in MDE, proved B refinements are also investigated in this paper in order to gradually translate abstract EMF models to concrete models which can then be automatically compiled into a programming language.

August 2020
DOI: 10.2495/CR200261
Conference: COMPRAIL 2020
Ning Liu, Wang KeMing, HOU XILIS, CHENG PENG

This article presents our experience in developing a tram control system using the B formal method.We find that there are some notable issues when using an abstract machine model to express softwaresystems and in automatic code generation, for which we have summarized the solutions. In this paper,we illustrate how to use the B module to develop complex systems, the rational choice of implicationrelations of the invariants, as well as the correctness of the variable definition in the model for codegeneration. The solutions to these issues can help developers with less experience to better use the Bmethod to develop the reliable systems.

September 2019
DOI: 10.1007/978-3-030-30942-8_44
In book: Formal Methods – The Next 30 Years
Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero Perez

Software in industrial products, such as in the railway industry, constantly evolves to meet new or changing requirements. For projects with a lifetime spanning decades (such as the control software for energy plants, for railway lines, etc.), keeping track of the original design rationale through time is a significant challenge.

September 2019
DOI: 10.3233/SAT190123
LicenseCC BY-NC 4.0
Tjark Weber, Sylvain Conchon, David Déharbe, Giles Reger

The International Satisfiability Modulo Theories Competition is an annual competitionbetween Satisfiability Modulo Theories (SMT) solvers. The 2018 edition of the competitionwas part of the FLoC Olympic Games, which comprised 14 competitions in various areas ofcomputational logic. We report on the design and selected results of the SMT Competitionduring the last FLoC Olympiad, from 2015 to 2018. These competitions set several newrecords regarding the number of participants, number of benchmarks used, and amount ofcomputation performed.

January 2019
DOI: 10.1007/978-3-030-18744-6_16
In book: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
Dalay Israel de Almeida Pereira, David Déharbe, Matthieu Perin, Philippe Bon

In the railway signalling domain, a railway interlocking sys-tem (RIS) is responsible for controlling the movement of trains by allow-ing or denying their routing according to safety rules. Relay diagrams area commonly used abstraction in order to model relay-based RIS, describ-ing these systems by graph-like schemata that present the connectionsbetween electrical components. The verification of these diagrams re-garding safety, however, is a challenging task, due to their complexityand the lack of tools for the automatic proof and animation. The anal-ysis of relay diagrams by a specialist is the main method to verify thecorrectness and the safety of these systems. Nonetheless, human man-ual analysis is error prone. This paper presents an approach for formallyspecifying the behaviour of the systems described in relay diagrams inthe B-method formal language. Considering that each relay has only twostates, it is possible to describe the rules for the state evolution of asystem by logical propositions. Furthermore, it is possible to use ProBin order to animate and model-check the specification

October 2019
PhD thesis
Tueno Fotso Steve Jeffrey

The SysML/KAOS method allows to model system requirements through goal hierarchies. B System is a formal method used to construct, verify and validate system specifications. A B System model consists of a structural part (abstract and enumerated sets, constants with their associated properties, and variables with their associated invariant) and a behavioral part (events). Correspondence links are established in previous work between SysML/KAOS and B System to produce a formal specification from requirements models. This specification serves as a basis for formal verification and validation tasks to detect and correct inconsistencies. However, it is required to manually provide the structural part of the B System specification.This thesis aims at enriching SysML/KAOS with a language that allows tomodel the application domain of the system and which would be compatible withthe requirements modeling language. This includes the definition of the domainmodeling language and of mechanisms for leveraging domain modeling to providethe structural part of the B System specification obtained from requirements models.The defined language uses ontologies to allow the formal representation of systemdomain. Moreover, the established correspondence links and rules, formally verified,allow both propagation and backpropagation of additions and deletions, betweendomain models and B System specifications. An important part of the thesis is alsodevoted to assessment of the SysML/KAOS method on case studies. Furthermore,since the systems naturally break down into subsystems (enabling the distribution ofwork between several agents: hardware, software and human), SysML/KAOS goalmodels allow the capture of assignments of requirements to subsystems responsibleof their achievement. This thesis therefore describes the mechanisms required toformally guarantee that each requirement assigned to a subsystem will be wellachieved by the subsystem, within the constraints defined by the high-level systemand subsystem specifications.The SysML/KAOS method, thus enriched, has been implemented within an opensource tool using the model federation platform Openflexo, and has been evaluated on various industrial scale case studies. It enables the formal verification of requirements and facilitates their validation by the various stakeholders, including those with less or no expertise in formal methods. However, both the specification of the body of B System events and domain model logical formulas (that give B System properties and invariants) and the formal assessment (verification and validation) of the specification can only be manual. They are time consuming and require experts in formal methods. But this is the price to pay to achieve a formal verification and validation of requirements.

January 2018
DOI: 10.1007/978-3-319-91271-4_32
In book: Abstract State Machines, Alloy, B, TLA, VDM, and Z
Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard

We propose an automation-friendly set theory for the B method. This theory is expressed using first order logic extended to polymorphic types and rewriting. Rewriting is introduced along the lines of deduction modulo theory, where axioms are turned into rewrite rules over both propositions and terms. We also provide experimental results of several tools able to deal with polymorphism and rewriting over a benchmark of problems in pure set theory (i.e. without arithmetic).

January 2018
DOI: 10.1007/978-3-319-91271-4_3
In book: Abstract State Machines, Alloy, B, TLA, VDM, and Z
Jean-Raymond Abrial

After more than 20 years since the publication of the book on B, and almost 10 years since the publication of the book on Event-B, the purposeof this short paper is to present some key points of these technologies.

October 2017
DOI: 10.1007/978-3-319-68499-4_10
Conference: International Conference on Reliability, Safety and Security of Railway Systems
Mathieu Comptier, David Déharbe, Julien Molinero PerezJ, Denis Sabatier

This paper describes a safety analysis effort on RATP’s communication-based train control (CBTC) system Octys. This CBTC is designed for multi-sourcing and brownfield deployment on an existing interlocking infrastructure. Octys is already in operation on several metro lines in Paris, and RATP plans its deployment on several other lines in the forthcoming years. Besides the size and complexity of the system, the main technical challenges of the analysis are to handle the existing interlocking functionalities without interfering with its design and to clearly identify the responsibilities of each subsystem supplier. The distinguishing aspect of this analysis is the emphasis put on intellectual rigor, this rigor being achieved by using formal proofs to structure arguments, then using the Atelier B tool to mechanically verify such proofs, encoded in the Event-B notation.

May 2016
DOI: 10.13140/RG.2.2.33148.16000
Conference: ABZ 2016 Linz – keynote
Thierry Lecomte

What happened with B and Atelier B during its 20-year life – from industry point of view.

January 2016
DOI: 10.1007/978-3-319-28934-2_2
Conference: International Workshop on Formal Aspects of Component Software
David Déharbe, Stephan Merz

This paper presents a formal development of an Isabelle/HOL theory for the behavioral aspects of artifacts produced in the design of software components with the B method. We first provide a formalization of semantic objects such as labelled transition systems and notions of behavior and simulation. We define an interpretation of the B method using such concepts. We also address the issue of component composition in the B method.

October 2016Lecture Notes in Computer Science
DOI: 10.1007/978-3-319-46750-4_12
Conference: 13th International Colloquium on Theoretical Aspects of Computing (ICTAC 2016)At: Taipei, Taiwan
Pierre Halmagrand

The B Method is a formal method mainly used in the railway industry to specify and develop safety-critical software. To guarantee the consistency of a B project, one decisive challenge is to show correct a large amount of proof obligations, which are mathematical formulae expressed in a classical set theory extended with a specific type system. To improve automated theorem proving in the B Method, we propose to use a first-order sequent calculus extended with a polymorphic type system, which is in particular the output proof-format of the tableau-based automated theorem prover Zenon. After stating some modifications of the B syntax and defining a sound elimination of comprehension sets, we propose a translation of B formulae into a polymorphic first-order logic format. Then, we introduce the typed sequent calculus used by Zenon, and show that Zenon proofs can be translated to proofs of the initial B formulae in the B proof system.

July 2015
DOI: 10.1007/978-3-319-21215-9_5
Conference: Test and ProofsAt: L’Aquila, ItalyVolume: LNCS 9154
Anamaria Martins Moreira, Cleverton Hentz, David Déharbe, Valerio Gutemberg Medeiros Jr

In this paper, we present a case study where two code generators for the B-Method were validated using software testing techniques. Our testing strategy is a combination of Grammar-Based Testing (GBT) and Model-Based Testing (MBT) techniques. The strategy consists of two steps. In the first step, grammar-based coverage criteria are used to generate a wide and meaningful set of test input models to validate the parsing capabilities of the code generators. In the second step, a MBT tool is used to validate the correctness of the output produced by these tools. The MBT tool generates a set of tests based on the same input model used by the code generation tools. The generated code is considered correct (consistent with the input model) if it passes this set of tests. Using this testing strategy, we were able to find problems in both code generation tools with moderate effort.

November 2015
DOI: 10.29007/14v7
Conference: 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)At: Suva, Fiji
Guillaume Bury, David Delahaye, Damien Doligez, Olivier Hermant

We introduce an encoding of the set theory of the B method using polymorphic types and deduction modulo, which is used for the automated verification of proof obligations in the framework of the BWare project. Deduction modulo is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We also present the associated automated theorem prover Zenon Modulo, an extension of Zenon to polymorphic types and deduction modulo, along with its backend to the Dedukti universal proof checker, which also relies on types and deduction modulo, and which allows us to verify the proofs produced by Zenon Modulo. Finally, we assess our approach over the proof obligation benchmark provided by the BWare project.

November 2015
DOI: 10.1007/978-3-319-25423-4_20
Conference: Formal Methods and Software Engineering – 17th International Conference on Formal Engineering MethodsVolume: LNCS 9407
Akram Idani, Yves Ledru

Several approaches dedicated to model access control policies (e.g. MDA-Security, SecureUML, UMLSec, etc.) have used the Model Driven Engineering paradigm in order to ensure a clear separation of business rules and constraints specific to a target technology. Their supporting techniques mainly focus on modeling and verification of security rules without taking into account the functional model of the application and its interaction with the security model. In order to take into account both models, we developed the B4MSecure platform. It is a Model Driven Engineering platform that allows to graphically model and formally reason on both functional and security models. It translates a UML class diagram associated to a SecureUML model into formal B specifications. The resulting B specifications follow the separation of concerns principles in order to be able to validate both models separately and then validate their interactions. This paper gives an overview of our platform.

July 2014
DOI: 10.1002/9781119002727.ch5
In book: Formal Methods Applied to Complex Systems
Thierry Lecomte

The B method was introduced at the end of the 1980s to produce software that is correct by construction. This chapter discusses the uses of B method for control-command systems for controlling platform doors of metro trains, and safety of microelectronic components. For several years now, the RATP in France has used platform doors on metro platforms to avoid passengers falling onto the track. A system of this kind is in use for the driverless SAET-METEOR metro. In parallel with its use for safety systems and software in railways, the B method has also been used in microelectronics and in chip cards for safety applications. One example of this is the development of a Java bytecode verifier by Gemplus, and another example is the validation of a secured operating system based on microkernels.

June 2014
Conference: 1st International Workshop about Sets and Tools (SETS 2014) At: Toulouse
Thierry Lecomte

Refining a B specification into an implementation can be a complex and time consuming process. This process can usually be separated in two distinct parts: the specification part, where the refinement is used to introduce new properties and specification details, and the implementation, where refinement is used to convert a detailed B specification into a B0 implementation. This article presents experience on the development and use of a refiner tool that automates the production of implementable models, in a number of industrial applications.

October 2014
B. Dantas, David Déharbe, S. Galvao, Valerio Gutemberg Medeiros Jr

This paper investigates the application of the B method,beyond the classical algorithmic level provided by the B0 sub-language, and presents re- finements of B models at a level of precision equivalent to assembly language. We claim and justify that this extension provides a more reliable software de- velopment process as it bypasses two of the less trustable steps in the applic- ation of the B method: code synthesis and compilation. The results presented in the paper have a value as a proof of concept and may be used as a basis to establish an agenda,for the development,of an approach,to build verifying compilers [Hoare 2005] based on the B method.

September 2014
DOI: 10.1007/978-3-319-15075-8_1
Conference: SBMF 2014At: MaceioVolume: 8941
Richard Bonichon, David Déharbe, Thierry Lecomte, Valerio Gutemberg Medeiros JrV

In this talk we describe a multi-platform code generator for the B method. In particular, we present a translation procedure from a large subset of the B language for implementations towards LLVM source code. This translation is defined formally as a set of rules defined recursively on the abstract syntax for B implementations. It already handles most elements of the B language and is being extended to the full language. We describe different strategies to validate the generated LLVM code.

January 2014
DOI: 10.4204/EPTCS.139.5
SourcearXiv
Valerio Gutemberg Medeiros Jr, David Déharbe

This paper presents BEval, an extension of Atelier B to improve automation in the verification activities in the B method or Event-B. It combines a tool for managing and verifying software projects (Atelier B) and a model checker/animator (ProB) so that the verification conditions generated in the former are evaluated with the latter. In our experiments, the two main verification strategies (manual and automatic) showed significant improvement as ProB’s evaluator proves complementary to Atelier B built-in provers. We conducted experiments with the B model of a micro-controller instruction set; several verification conditions, that we were not able to discharge automatically or manually with AtelierB’s provers, were automatically verified using BEval.

June 2014
DOI: 10.1007/978-3-662-43652-3_10
Conference: ABZ 2014 Conference
Rahma Ben Ayed, Simon Collart-Dutilleul, Philippe Bon, Yves Ledru

The B method is a formal specification method and a means of formal verification and validation of safety-critical systems such as railway systems. In this short paper, we use the B4MSecure tool to transform the UML models, fulfilling requirements of European Railway Traffic Management System (ERTMS) operating rules, into B specifications in order to formally validate them.

July 2014
DOI: 10.1002/9781119002727.ch4
In book: Formal Methods Applied to Complex Systems
Daniel Dolle

Siemens SAS Industry Mobility is an international center of excellence for the creation of fully automatic subway systems and is a world leader in automated urban transport systems. The classic software development cycle involves specification, design, coding, testing and maintenance phases. These documents are translated into a formal model using B [ABR 96], known as the abstract model. The purpose of reviews is to identify faults in B models and their documentation as early as possible. Monitoring and analysis activities are also carried out with each evolution of Atelier B and the relevant transcoding tools. The implementation of automatic refinement has allowed us to multiply the size and complexity of our applications by 4, while reducing the size of development teams and the time needed to create our systems.

September 2013
DOI: 10.1007/978-3-642-40561-7_10
Conference: International Conference on Software Engineering and Formal Methods
Sebastian Krings, Michael Leuschel

Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated tools lack support for annotating variables with (physical) units of measurement. There is thus no obvious way to reason about correct or incorrect usage of such units. In this paper we present a technique that analyses the usage of physical units throughout a B machine, infers missing units and notifies the user of incorrectly handled units. The technique combines abstract interpretation with classical animation and model checking and has been integrated into the ProB validation tool, both for classical B and for Event-B. It provides source-level feedback about errors detected in the models. The plugin uses a combination of abstract interpretation and constraint solving techniques. We provide an empirical evaluation of our technique, and demonstrate that it scales up to real-life industrial models.

February 2012
Thierry Lecomte, Lilian Burdy, Jean-Louis Dufour

For a long time, formal methods have ignored floating-point computations. About ten years ago this has changed, and today specification languages and tools are in use in research and preindustrial contexts. Better late than never: the B method, which has been the first formal method to prove real-size software, will soon be able to prove the correctness of floating-point computations. This paper gives the motivations, the philosophy and the first impacts on the AtelierB tool.

September 2012
DOI: 10.1007/978-3-642-33296-8_4
Conference: Proceedings of the 15th Brazilian conference on Formal Methods: foundations and applications
Haniel Barbosa, David Déharbe

This paper presents an approach to verify PLCs, a common platform to control systems in the industry. We automatically translate PLC programs written in the languages of the IEC 61131-3 standard to B models, amenable to formal analysis of safety constraints and general structural properties of the application. This approach thus integrates formal methods into existing industrial processes, increasing the confidence in PLC applications, nowadays validated mostly through testing and simulation. The transformation from the PLC programs to the B models is described in detail in the paper. We also evaluate the approach’s potential with a case study in a real railway application.

June 2012
DOI: 10.1007/978-3-642-30885-7_30
Conference: Proceedings of the Third international conference on Abstract State Machines, Alloy, B, VDM, and Z
Haniel Barbosa, David Déharbe

In this paper we propose an approach to verify PLC programs, a common platform to control systems in the industry. Programs written in the languages of the IEC 61131-3 standard are automatically translated to B machines and are then amenable to formal analysis of safety constraints and general structural properties of the application. This approach thus integrates formal methods into existing industrial processes.

October 2012
DOI: 10.1145/2427376.2427379
Conference: Proceedings of the Workshop on Model-Driven Engineering, Verification and Validation
Erwan Bousse, David Mentré, Benoît Combemale, Takaya Katsuragi

Systems engineering, and especially the modeling of safety critical systems, needs proper means for early Validation and Verification (V&V) to detect critical issues as soon as possible. The objective of our work is to identify a verifiable subset of SysML that is usable by system engineers, while still amenable to automatic transformation towards formal verification tools. As we are interested in proving safety properties expressed using invariants on states, we consider the B method for this purpose. Our approach consists in an alignment of SysML concepts with an identified subset of the B method, using semantic similarities between both languages. We define a restricted SysML extended by a lightweight profile and a transformation towards the B method for V&V purposes. The obtained process is applied to a simplified concrete case study from the railway industry: a SysML model is designed with safety properties, then automatically transformed into B, and finally imported into Atelier-B for automated proof of the properties.

February 2010
DOI: 10.1007/978-3-642-11811-1_45
SourceDBLP
Conference: Proceedings of the Second international conference on Abstract State Machines, Alloy, B and Z
Alessandro Gurgel, Valerio Gutemberg Medeiros Jr, Marcel V M Oliveira, David Déharbe

An important frequent task in both Z and B is the proof of verification conditions (VCs). In Z and B, VCs can be predicates to be discharged as a result of refinement steps, some proof about initialization properties or domain checking. Ideally, a tool that supports any Z and B technique should automatically discharge as many VCs as possible. Here, we present ZB2SMT, a Java package designed to clearly and directly integrate both Z and B tools to the satisfiability module theory (SMT) solvers such as veriT [1], a first-order logic (FOL) theorem prover that accepts the SMT syntax [4] as input. By having the SMT syntax as target we are able to easily integrate with further eleven automatic theorem provers. ZB2SMT is currently used by Batcave [2], an open source tool that generates VCs for the B method and CRefine [3], a tool that supports the Circus refinement calculus. Much of the VCs generated to validate the refinement law applications, are based on FOL predicates. Hence, CRefine uses the ZB2SMT package to automatically prove such predicates. The package integrates elements of Z and B predicates in a common language and transforms these predicates into SMT syntax. In this process, a SMT file is generated containing the predicate and some definitions. It is sent to a chosen SMT solver which yields a Boolean value for the predicate or it can be sent to several SMT solvers in a parallel approach. In order to improve the performance of the proof system, ZB2SMT has a module that can call different instances of solvers at different computers, according to a configuration file. It improves the proof process by allowing different strategies to be performed in parallel, reducing the verification time.

August 2009
DOI: 10.1007/978-3-642-10452-7_19
Conference: Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers
Valério Medeiros Júnior, David Déharbe

This paper describes an approach to model the functional aspects of the instruction set of microcontroller platforms using the no- tation of the B method. The paper presents specifically the case of the Z80 platform. This work is a contribution towards the extension of the B method to handle developments up to assembly level code.

August 2009
DOI: 10.1007/978-3-642-10452-7_8
SourceDBLP
Conference: Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers
David Déharbe, Stephenson Galvão, Anamaria Martins Moreira

This paper presents the current state of the formal development of FreeRTOS, a real-time operating system. The goal of this effort is to address a scientific challenge and is realized within the scope of the Grand Challenge on Verified Software. The development is realized with the B method. A model of the main functionalities of the FreeRTOS is now available and can be a starting point to establish an agreed formal specification of FreeRTOS that can be used by the research community.

July 2009
SourcearXiv
David Déharbe, Bruno E. G. Gomes, Anamaria Martins Moreira

Model-driven design of software for safety-critical applications often relies on mathematically grounded techniques such as the B method. Such techniques consist in the successive applications of refinements to derive a concrete implementation from an abstract specification. Refinement theory defines verification conditions to guarantee that such operations preserve the intended behaviour of the abstract specifications. One of these conditions requires however that concrete operations have exactly the same signatures as their abstract counterpart, which is not always a practical requirement. This paper shows how changes of signatures can be achieved while still staying within the bounds of refinement theory. This makes it possible to take advantage of the mathematical guarantees and tool support provided for the current refinement-based techniques, such as the B method. Comment: 18 pages, submitted to ICFEM 2009

July 2009Electronic Notes in Theoretical Computer Science 240:79-96
DOI: 10.1016/j.entcs.2009.05.046
Bartira Dantas, David Déharbe, Stephenson Galvão, Valerio Gutemberg Medeiros JrV

This paper investigates the application of the B method beyond the classical algorithmic level provided by the B0 sub-language, and presents refinements of B models at a level of precision equivalent to assembly language. We claim and justify that this extension provides a more reliable software development process as it bypasses two of the less trustable steps in the application of the B method: code synthesis and compilation. The results presented in the paper have a value as a proof of concept and may be used as a basis to establish an agenda for the development of an approach to build verifying compilers [Hoare, C. A. R., The verifying compiler, a grand challenge for computing research, in: VMCAI, 2005, pp. 78–78] based on the B method.

September 2008
DOI: 10.1007/978-3-540-87603-8_39
Conference: Abstract State Machines, B and Z, First International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings
David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira

A smart card is a portable computer device able to store data and execute commands. Java Card [1] is a specialization of Java, providing vendor inter-operability for smart cards, and has now reached a de facto standard status in this industry. The strategic importance of this market and the requirement for a high reliability motivate the use of rigorous software development processes for smart card aware applications based on the Java Card technology. The B method [2] is a good candidate for such process, since it is a formal method with a successful record to address industrial-level software development. In [3,4], we proposed two versions of a Java Card software development method (called BSmart) based on the B method. The main feature of these methods is to abstract the particularities of smart card systems to the applications developers as much as possible. This abstract presents the current version of a tool, also called BSmart, to support the method. The tool provides the automatable steps required by the method and some guidelines and library machines that are useful during the development process. It includes B development tools (type checker, PO generator) and specific BSmart tools (refinement generator, Java Card translator, etc.). In this approach, the card services specifier only needs to apply some refinement steps to his abstract (implementation platform independent) B specification. The generation of these refinements adapts the specification to Java Card standards and introduces platform specific aspects gradually. Finally, from the concrete B refinements the Java Card code implementing the services provided by the card will be automatically generated by the tool. The tool also provides the generation of a Java API for the host-side application from the original abstract specification, encapsulating all the communication protocol details. Thus, the client application code can then be developed in a completely platform independent way. The definition of the method is in a mature stage, and our attention is now focused on the implementation of more robust versions of the BSmart tools and packaging them in a user-friendly environment. The integration of verification and animation tools is also planned for a next release of the tool.

January 2007
Thierry Lecomte, Dominique Mery, Dominique Cansell

Designers can now justify their design decisions based on the patterns they have applied. Just as the quality of a source code can easily be judged by a quick look at the coding standards that have been followed, the quality of a design can now be judged by the patterns used. These concepts are transferable to the field of system design, especially from the point of view of their verification and validation. Refinement is a tool for correct systems engineering. However, this tool, like many others, requires expert use to be effective. Such expertise must be catalogued and reused, where possible, in the form of design patterns. These patterns should focus on verification and formal validation, to provide high-level tools that can be used to justify the achievement of security and trust objectives. Building such patterns requires theoretical innovations, and we believe that formal design patterns or proven design patterns will play a vital role in the verification-based measurement of the achievement of security and trust objectives. Proven design patterns have a very interesting feature: they are built according to a devalidation goal of the designed objects and capture the proof-oriented information of the system under construction. First results have been obtained in the study of reactive systems (INRS) and the EAL5+ certification of smart card security policies.

July 2007Electronic Notes in Theoretical Computer Science 184:81-96
DOI: 10.1016/j.entcs.2007.03.016
Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira, David Déharbe

This work proposes a methodology for the rigorous development of Java Card smart card applications, using the B Method. Its main feature is to abstract the particularities of Java Card and smart card aware applications from the specifier as much as possible. In the proposed approach, the specification of the aplication logic needs not be preoccupied with the specific aspects of the Java Card platform (in particular, communication between the card acceptance device and the smart card itself). Platform-specific code can then be automatically generated during the refinement and code generation process. An interesting side-effect of this approach is that the specification may be reused with any other platform of implementation.

January 2006
DOI: 10.1007/BFb0020001
In book: VDM ’91 Formal Software Development Methods
Jean-Raymond Abrial, Matthew K. O. Lee, D. S. NeilsonShow, H. Sørensen

The B-method is designed to provide a homogeneous language and a methodology for the formal specification, design and implementation of real-life software systems. Therefore, the features of incremental construction and proof have been guiding principles in its development. A full account of the B-method and its theoretical foundations is to appear shortly as a book by J.-R. Abrial. An environment, the B Toolkit, supports formal development activities from specification to coding. The toolkit itself is supported by a platform, the B-tool, which is now commercially available from Edinburgh Portable Compilers Ltd. The B Toolkit will soon be ready for alpha testing, and it is planned to make it commercially available in due course.

November 2004Journal of the Brazilian Computer Society 9(2):17-36
DOI: 10.1590/S0104-65002003000300003
Jean-François Couchot, David Déharbe, Alain Giorgetti, Silvio Ranise

We present a technique to prove invariants of model-based specications in a fragment of set theory. Proof obligations containing set theory constructs are translated to first-order logic with equality augmented with (an extension of) the theory of arrays with extensionality. The idea underlying the translation is that sets are represented by their characteristic function which, in turn, is encoded by an array of Booleans indexed on the elements of the set. A theorem proving procedure automating the verication of the proof obligations obtained by the translation is described. Furthermore, we discuss how a sub-formula can be extracted from a failed proof attempt and used by a model finder to build a counter-example. To be concrete, we use a B specification of a simple process scheduler on which we illustrate our technique.