Bibliographie

La méthode formelle B est une méthode de développement logicielle industrielle qui a motivé des travaux de recherche depuis les années 1990. Vous trouverez ci-dessous une liste non exhaustive de travaux publiés relatifs au développement de logiciels sûrs, à la modélisation formelle avec B et Event-B, à la preuve mathématique de ces modèles, à la preuve de spécification système ainsi qu’à la programmation de la CLEARSY Safety Platform avec B.

 

2023

Teaching and Training in Formalisation with B

February 2023
DOI: 10.1007/978-3-031-27534-0_6
Conference: Formal Methods Teaching. FMTea 2023. Lübeck
Thierry Lecomte

 

Despite significant advancements in the design of formal integrated development environments, applying formal methods in software industry is still perceived as a difficult task. To ease the task, providing tools that help during the development cycle is essential but proper education of computer scientists and software engineers is also an important challenge to take up. This paper summarises our experience of 20 years spent in the education of engineers, either colleagues or customers, and students, together with the parallel design and improvement of supporting modelling tools.

2022

Safe and Secure Architecture Using Diverse Formal Methods

October 2022
DOI: 10.1007/978-3-031-19762-8_24
In book: Leveraging Applications of Formal Methods, Verification and Validation. Practice
Thierry Lecomte

The distribution of safety functions along the tracks requires the networking of the ECUs (Electronic Control Unit is an embedded system that controls one or more electrical systems or subsystems) that support them, to facilitate their operation and maintenance. The latter enables logs to be sent, commands to be received and sent that will lead to a state change of one of the connected equipment, and the ECU application software to be updated. All these activities are naturally subject to targeted attacks aimed at reducing the availability of the equipment or disrupting its operational safety to the point of creating accidents. This article presents an innovative approach partitioning security and safety on two different computers. One computer connected to the network ensures security and is regularly updated according to known threats. The other computer ensures safety and communicates only through a secure filter. Each computer embeds technological elements that have been specified, implemented and proven with 2 different formal methods.

Standardisation Considerations for Autonomous Train Control

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 .

Assigning Safe Executed Systems to Meanings

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.

The B Method meets MDE: Review, progress and future

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.

Debugging Support in Atelier B

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.

2021

Digital Modelling in the Railways

August 2021
DOI: 10.1007/978-3-030-83723-5_9
In book: Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends, 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV
Thierry Lecomte

The railways have a quite long modelling history, covering many technical aspects from infrastructure to rolling stock, train movement, maintenance, etc. These models are mostly separate and operated independently by various stakeholders and with diverse objectives. This article presents some of the various digital modelling activities, including formal ones, that are undertaken by the railway industry, for design, development, validation, qualification, and exploitation. It also introduces trends toward regrouping models to obtain more significant results together with a larger scope, prefiguring digital twins.

2020

The CLEARSY safety platform: 5 years of research, development and deployment

August 2020, Science of Computer Programming 199:102524

DOI: 10.1016/j.scico.2020.102524

 Thierry Lecomte, David Déharbe, Paulin Fournier, Marcel V M Oliveira

The CLEARSY Safety Platform (CSSP) was designed to ease the development of safety critical systems and to reduce the overall costs (development, deployment, and certification) under the pressure of the worldwide market. 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 and cannot be altered by the developer. Summarizing a 5-year return of experience in the effective application in the railways, this article explains how this approach is a game-changer and tries to anticipate the future of this platform for safety critical systems. In particular, the education of future engineers and the seamless integration in existing engineering processes with the support of Domain Specific Languages are key topics for a successful deployment in other domains. DSL like Robosim to program mobile robots and relay circuits to design railway signalling systems are connected to the platform.

The First Twenty-Five Years of Industrial Use of the B-Method

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.

Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B

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.

Applying a Formal Method in Industry: a 25-Year Trajectory

May 2020
LicenseCC BY 4.0
Thierry Lecomte, David Déharbe, Étienne Prun, Erwan Mottin

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. Hence the feedback provided by industry to academics is not as constructive as it might be. Summarizing a 25-year return of experience in the effective application of a formal method – namely B and Event-B – in diverse application domains (railways, smartcard, automotive), this article makes clear why and where formal methods have been applied, explains the added value obtained so far, and tries to anticipate the future of these two formalisms for safety critical systems.

Low Cost High Integrity Platform

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).

A Safety Flasher Developed with the CLEARSY Safety 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.

The Bourgeois Gentleman, Engineering and Formal Methods

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.

Programming the CLEARSY Safety Platform with B

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.

Alliance of model-driven engineering with a proof-based formal approach

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.

Application exploration of B method in the development of safety-critical control systems

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.

2019

BTestBox: A Tool for Testing B Translators and Coverage of B Models

September 2019
DOI: 10.1007/978-3-030-31157-5_6
In book: Tests and Proofs
Diego De Azeve do Oliveira, Valério Medeiros, David Déharbe, Martin Musicante

The argument of correctness in refinement-based formal software design often disregards source code analysis and code generation. To mitigate the risk of errors in these phases, certifications issued by regulation entities demand or recommend testing the generated software using a code coverage criteria. We propose improvements for the BTestBox, a tool for automatic generation of tests for software components developed with the B method. BTestBox supports several code coverage criteria and code generators for different languages. The tool uses a constraint solver to produce tests, thus being able to identify dead code and tautological branching conditions. It also generates reports with different metrics and may be used as an extension to the Atelier B. Our tool performs a double task: first, it acts on the B model, by checking the code coverage. Second, the tool performs the translation of lower level B specifications into programming language code, runs tests and compares their results with the expected output of the test cases. The present version of BTestBox uses parallelisation techniques that significantly improve its performance. The results presented here are encouraging, showing performance numbers that are one order of magnitude better than the ones obtained in the tool’s previous version.

Property-Driven Software Analysis: (Extended Abstract)

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.

The SMT Competition 2015–2018

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.

B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution

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

Towards a tooled and proven formal requirements engineering approach

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.

2018

The Atelier B Proof System and Its Improvements

November 2018
DOI: 10.13140/RG.2.2.35928.52480
Conference: ETMF 2018, Salvador, 26 Novermber 2018
Thierry Lecomte

Presentation of the Atelier B proof system:

  • intro to the B method
  • proof system
  • improvements

given at the occasion of the Escola de Informática Teórica e Métodos Formais (ETMF)

An Automation-Friendly Set Theory for the B Method

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).

On B and Event-B: Principles, Success and Challenges

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.

2017

Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa"

January 2017
DOI: 10.4204/EPTCS.240.6
Project: Machine assisted verification for proof obligations stemming from formal methods.
Lilian Burdy, David Déharbe, Étienne Prun

The application of automatic theorem provers to discharge proof obligations is necessary to apply formal methods in an efficient manner. Tools supporting formal methods, such as Atelier~B, generate proof obligations fully automatically. Consequently, such proof obligations are often cluttered with information that is irrelevant to establish their validity. We present iapa, an « Interface to Automatic Proof Agents », a new tool that is being integrated to Atelier~B, through which the user will access proof obligations, apply operations to simplify these proof obligations, and then dispatch the resulting, simplified, proof obligations to a portfolio of automatic theorem provers.

Safety Analysis of a CBTC System: A Rigorous Approach with Event-B

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.

2016

Double cœur et preuve formelle pour automatismes SIL4

December 2016
DOI: 10.4267/2042/61819
Conference: Congrès Lambda Mu 20 de Maîtrise des Risques et de Sûreté de Fonctionnement, 11-13 Octobre 2016, Saint Malo, France
Thierry Lecomte

The bi-processor secure architecture combine software and hardware techniques, compatible with EN5012{6, 8, 9}, and allows todesign low cost, high integrity automatisms. This smart architecture combines formal software development with proof andsimple, secure execution platform. This architecture has been applied to several industrial settings and is being improved and made generic through a collaborative research and development project.

Atelier B has turned 20

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.

Software Component Design with the B Method — A Formalization in Isabelle/HOL

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.

Soundly Proving B Method Formulæ Using Typed Sequent Calculus

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.

2015

Formal Virtual Modelling and Data Verification for Supervision Systems

June 2015
DOI: 10.1007/978-3-319-19249-9_41
Conference: FM 2015 – Industry Track At: Oslo
Thierry Lecomte

This paper reports on the use of formal techniques to ensure as far as possible a safe decommissioning of a plant several decades after it was designed and built. Combination of supervised learning, formal modelling, model animation and model checking enabled the recovery of an almost lost specification and the design of a virtual supervision system that could be checked against recorded plant data.

Verifying Code Generation Tools for the B-Method Using Tests: A Case Study

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.

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo

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.

B for Modeling Secure Information Systems - The B4MSecure Platform

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.

Spécification, construction et vérification de programmes : le parcours d'une pensée scientifique sur une quarantaine d'années

April 2015
Vidéo
Conférence: Collège de France
Jean-Raymond Abrial

Cette présentation vidéo est celle d’un chercheur vieillissant qui porte un regard historique sur les quarante dernières années de son travail.

Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques. Je fais partie de la seconde catégorie, car j’ai toujours pratiqué le même genre d’investigations, à savoir la spécification et la construction vérifiée de systèmes informatisés.

Ce travail, autant théorique que pratique, s’est concrétisé au cours de toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas, loin de là, le seul contributeur). Je vais tenter d’expliciter comment les idées que contiennent ces formalismes et les outils correspondants ont lentement émergés de façon parfois erratique.

Je tenterai aussi de préciser les multiples influences qui ont participé à cette évolution. En particulier, je montrerai comment plusieurs réalisations industrielles ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et parfois les rejets de la part de communautés tant universitaires qu’industrielles.

Pour finir, je proposerai quelques réflexions et approches pour le financement de recherches telles que celle-ci.

2014

LLVM-based code generation for B

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

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.

Industrial Applications for Modeling with the B Method

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.

Return of Experience on Automating Refinement in B

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.

Applying the B Method to Take on the Grand Challenge of Verified Compilation

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.

LLVM-based code generation for B

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.

BEval: A Plug-in to Extend Atelier B with Current Verification Technologies

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.

B Formal Validation of ERTMS/ETCS Railway Operating Rules

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.

The B Method at Siemens

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.

2013

Integration of SMT-solvers in B and Event-B development environments

March 2013Science of Computer Programming 78(3):310-326
DOI: 10.1016/j.scico.2011.03.007
Project: Machine assisted verification for proof obligations stemming from formal methods.
David Déharbe

Software development in B and Event-B generates proof obligations that have to be discharged using theorem provers. The cost of such developments depends directly on the degree of automation and efficiency of theorem proving techniques for the logics in which these lemmas are expressed. This paper presents and formalizes an approach to transform a class of proof obligations essentially similar to those generated in the Rodin platform into the input language of a category of automatic theorem provers known as SMT-solvers. The work presented in the paper handles proof obligations with Booleans, integer arithmetics, basic sets and relations and has been implemented as a plug-in for Rodin.

Inferring Physical Units in B Models

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.

2012

Formally Checking Large Data Sets in the Railways

October 2012
Source arXiv
Thierry Lecomte, Lilian Burdy, Michael Leuschel

This article presents industrial experience of validating large data sets against specification written using the B / Event-B mathematical language and the ProB model checker.

The B method takes up floating-point numbers

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.

An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting

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.

Formal Verification of PLC Programs Using the B Method

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.

Aligning SysML with the B Method to Provide V&V for Systems Engineering

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.

2011

B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design

September 2011
DOI: 10.1007/978-3-642-25032-3_4
SourceDBLP
Conference: Formal Methods, Foundations and Applications – 14th Brazilian Symposium, SBMF 2011.At: São Paulo, Brazil
Marcel V M Oliveira, David Déharbe, Luís C. D. S. Cruz

This paper presents a migration approach from a class of hierarchical B models to CSP. The B models follow a so-called polling pattern, suitable for reactive systems, and are automatically translated into a set of communicating CSP processes with the same behaviour. The structure of the CSP model matches that of the B model and may be formally analysed using model checking. Selected CSP processes may then be further refined and synthesised to hardware, while the remaining modules would be mapped to software using B refinements. The translation proposed here paves the way for a model-based approach to hardware and software co-design employing complementary formal methods.

2010

Applying the B Method for the Rigorous Development of Smart Card Applications

February 2010
DOI: 10.1007/978-3-642-11811-1_16
Conference: Abstract State Machines, Alloy, B and Z, Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings
Bruno Emerson Gurgel Gomes, David Déharbe, Anamaria Martins Moreira, Katia Moraes

Smart Card applications usually require reliability and security to avoid incorrect operation or access violation in transactions and corruption or undue access to stored information. A way of reaching these requirements is improving the quality of the development process of these applications. BSmart is a method and a corresponding tool designed to support the formal development of the complete Java Card smart card application, following the B formal method.

Integrating SMT-Solvers in Z and B Tools

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.

2009

Applying a Formal Method in Industry: A 15-Year Trajectory

November 2009
DOI: 10.1007/978-3-642-04570-7_3
Conference: Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems
Thierry Lecomte

This article presents industrial experience of applying the B formal method in the industry, on diverse application fields (railways, automotive, smartcard, etc.). If the added value of such an approach has been demonstrated over the year, using a formal method is not the panacea and requires some precautions when introduced in an industrial development cycle.

Formal Modelling of a Microcontroller Instruction Set in B

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.

Formalizing FreeRTOS: First Steps

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.

Refining interfaces: the case of the B method

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

Verified Compilation and the B Method: A Proposal and a First Appraisal

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.

2008

Safe and Reliable Metro Platform Screen Doors Control/Command Systems

May 2008
DOI: 10.1007/978-3-540-68237-0_32
Conference: FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008, Proceedings
Thierry Lecomte

In this article we would like to present some recent applications of the B formal method to the development of safety critical system. These SIL3/SIL4 1 compliant systems have their functional specification based on a formal model. This model has been proved, guaranteeing a correct by construction behaviour of the system in absence of failure of its components. The constructive process used during system specification and design leads to a high quality system which has been qualified 2 by French authorities.

BSmart: A Tool for the Development of Java Card Applications with 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.

2007

Formal Methods in Safety-Critical Railway Systems

August 2007
Conference: SBMF
Thierry Lecomte, Thierry Servat, Guilhem Pouzancre

In this article we would like to present some recent applications of the B formal method to the development of safety critical systems, namely platform screen door controllers. These SIL3/SIL4 1 compliant systems have their functional specification based on a formal model. This model has been proved, guaranteeing a correct by construction behaviour of the system in absence of failure of its components. The constructive process used during system specification and design leads to a high quality system which has been qualified 2 by French authorities.

Patrons de conception prouvés

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.

Developing Java Card Applications with B

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.

2006

Automation of Java Card component development using the B method.

January 2006
DOI: 10.1109/ICECCS.2006.51
Conference: 11th International Conference on Engineering of Complex Computer Systems (ICECCS 2006), 15-17 August 2006, Stanford, California, USA
David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira

This paper presents a method 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 application logic does not need to take into account the specific aspects of the Java Card platform (in particular, communication between the card acceptance device and the smart card itself). A sequence of preestablished refinements is then applied to the original specification to yield an implementation-level B description of the component, which can then be used to synthesize Java Card code. This method reduces significantly the required amount of user-interaction and improves productivity. An interesting side-effect of this approach is that the specification may be reused with any other platform of implementation.

The B-method

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.

2004

A hardware/software codesign framework for developing complex embedded systems using formal model refinement.

January 2004
Conference: Forum on specification and Design Languages, FDL 2004, September 14-17, 2004, Lille, France, Proceedings
Nikos S. Voros, Colin Snook, Stefan Hallerstede,  Thierry Lecomte

Scalable Automated Proving and Debugging of Set-Based Specifications.

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.

2002

Event driven B: methodology, language, tool support, and experiments

ClearSy, in close collaboration with J.R. Abrial and Louis Mussat (DCSSI). The main objective has been to verify suitability of B for system modelling. Most of these activities have been funded by MATISSE project (IST-1999-11435).