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.

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.

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.

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.

We present b2llvm, a multi-platform code generator for the B-method. The b2llvm code generator currently handles the following elements of the B language: simple data types, imperative instructions and component compositions. In particular, this paper describes a translation for essential implementation constructs of the B language into LLVM source code, implemented into the b2llvm compiler. We use an example-based approach for this description.

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

Use Cases (UC) are a popular way of describing system behavior and UC quality impacts the overall system quality. However, they are presented in natural language, which is usually the cause of issues related to imprecision, ambiguity, and incompleteness. We present the results of an empirical study on the formalization of UCs as Graph Transformation models (GTs) with the goal of running tool-supported analyses on them and revealing possible errors. To evaluate our approach, we apply it to a set of real UC descriptions obtained from a software developer company and measured the results through metrics. The final results demonstrate that this approach can reveal real problems that could otherwise go undetected and, thus, help improve the quality of the UCs.

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.

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.

Methods exploiting problem symmetries have been very successful in several areas including constraint programming and SAT solving. We here recast a technique to enhance the performance of SMTsolvers by detecting symmetries in the input formulas and use them to prune the search space of the SMT algorithm. This technique is based on the concept of (syntactic) invariance by permutation of constants. An algorithm for solving SMT by taking advantage of such symmetries is presented. The implementation of this algorithm in the SMT-solver veriT is used to illustrate the practical benefits of this approach. It results in a significant improvement of veriT's performances on the SMTLIB benchmarks that places it ahead of the winners of the last editions of the SMT-COMP contest in the QF-UF category.

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.

We introduce a condition for the verification of properties in component-based systems that allows for components with variants and hence supports reusability. Thereby, the architecture of the system and behavior equivalences between the components are exploited in order to cope with the state space explosion problem. We use the model of interaction systems as the component model and extend it with unobservable behavior and a new composition operator.

This article describes the first public version of the satisfiability modulo theory (SMT) solver veriT. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.

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.

SMT (Satisfiability Modulo Theories) solvers are automatic verification engines suitable to discharge important classes of proof obligations generated in applying formal construction of software and hardware designs. In this paper, we present a new approach to combine decision procedures and propositional solvers into an SMT-solver. This approach is based on the generation of model equalities by decision procedures. We show the soundness and completeness of the proposed approach using an original abstract framework to represent and reason about SMT-solvers. We then present an algorithmic version of the new SMT-solving approach and discuss practical aspects of our implementation.

This paper describes an approach to model the functional aspects of the instruction set of microcontroller platforms using the notation 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.

Declarative techniques for software verification require the availability of scalable, predictable, and flexible satisfiability solvers. We describe our approach to build such solvers by combining equational theorem proving, Boolean solving, arithmetic reasoning, and some transformations of the proof obligations. The proposed techniques have been implemented in a system called haRVey and the viability of the approach is shown on proof obligations generated in the certification of aerospace code.

Mutual exclusion locks have traditionally been used for synchronizing the access of multiple processes to shared data structures. Multi-processor architectures offer new synchronization primitives that have given rise to algorithms for optimistic concurrency and non-blocking implementations. These algorithms are quite subtle and raise the need for formal verification. We propose a refinement-based method for designing and verifying non-blocking, and in particular lock-free, algorithms. We achieve good success in automatically discharging the verification conditions generated by this method, relying on first-order and SMT provers, augmented by a simple but useful instantiation heuristic. We present our method using a non-trivial running example due to Harris et al.