In 2023, the Professional version will be updated twice, through a corrective version in Q1 2023 and an evolutionary version in Q3 2023 with the display of counter-examples in the proof interface. In 2024, the T2 EN50128 and IEC 61508 certified Professional version will be made available, as well as the Community version integrating a RUST code generator.
List of corrections for the Professional version Q1 2023:
- More powerful automatic checking of proof rules Packing of pup file to a project resource
- Launching bbatch on a given workspace is made easier
- Archiving in Windows fixed Arguments to the `bb` (loop) command in an interactive proof are now saved in the correct order.
- Improved type inference in the B compiler
- Fixed the Linux installer to avoid failures in newer distributions
- Fixed constant values in the pptranssmt translator
- The size of the horizontal scroll bar in the proof tree is now correct.
- XML output from bbatch for the `gs` interactive prover command is now well balanced
- The GUI does not crash when receiving corrupted XML data from bbatch as part of internal interactions; instead, it produces diagnostic information.
- Improved assumption selection in the `pptranssmt` translator.
- `Force(Fast)` is now handled for projects in NG mode (i.e, in `pos` format)
- The `iterate` operator is now correctly rendered from the proof obligation view in the component editor.
- Correction in rules created by the SMT hammer in the interactive proof.
- Improved support for operation calls and inlined imports in NGOP
- Fixed an encoding issue in the proof mechanism writer `ppTransSmt`
- Added support for various B operators in the proof mechanism writer `ppTransSmt`
- Checking for B0 conditions in the type check phase is disabled for system projects.
- Documentation for Event-B support has been updated with closure implementations (syntax and proof obligations).
- Error messages displayed in the component editor can be copied to the clipboard.
- The dialog for saving interactive proofs in the `User_Pass` theory now includes checkboxes for saving to the PMM component file, the PUP component file, or the PatchProver project file.
- Added setting to display the host name in the main window title
- Added custom proof obligation generator for optional Event-B proof obligations
- The user can now undo the closure of the interactive prover (if interactive proof commands have been issued).
List of corrections for the Professional version Q3 2023:
- Display of counterexamples in the modelling and proof interface. When using the formal B method, design errors correspond to invalid proof obligations. Atelier B automatic provers are not able to identify whether a proof failure is due to a logical error, whereas SMT solvers are able to prove a first-order logic formula but also to refute it and produce a counterexample. These counterexamples can give the user valuable insights into design errors. SMT solvers have been integrated into the most recent version of Atelier B, but only to use their proof capabilities.
3 Novembre 2009 à Eindhoven
Le workshop « Recent Innovations and Applications in B » (RIAB) aura lieu le 3 novembre 2009 durant le Formal Methods Weeket aura lieu dans l’auditorium de la Technische Universiteit Eindhoven.
Supporté par les deux principales plateformes de modélisation open-source (RODIN et Atelier B), et en relation avec un nombre grandissant d’utilisations industrielles dans le domaine du ferroviaire, et des cartes à puces, ce workshop vise à reproduire une photographie de l’état de développement et de dissémination de B et du B événementiel. L’accent sera mis sur les applications industrielles (depuis les cas d’études jusqu’aux implémentations lourdes) et sur la recherche appliquée. Le workshop incluera une large palette de présentations données par des membres du projet DEPLOY, des industriels, et des chercheurs.
|09:00||Event B recipes for proof-based design of distributed systems||Dominique Méry (Université Henri Poincaré Nancy 1, LORIA)|
|09:30||A proved « correct by construction » realistic digital circuit||Marc Benveniste (STMicroelectronics)|
|11:00||ProB for Validating Large Scale Railway Models||Michael Leuschel (University of Düsseldorf)|
|11:30||Automatic refinement and code generation: lessons learned||Thierry Lecomte (CLEARSY)|
|12:00||Formal Modeling Feedback on Train Tracking||Mathieu Clabaut (Systerel)|
|14:00||Event-B in Space – or are we still on the ground?||Dubravka Ilic (Space Systems Finland)|
|14:30||Formal Development of Enterprise Service Communication||Andreas Roth (SAP AG)|
|15:00||Formal Methods Outside the Mother Land||Aryldo G Russo Jr. (AeS Group & Research Institute of State of Sao Paulo)|
|16:00||Probabilities in event-B for railways safety critical systems||Jérôme Falampin (Siemens Transportation Systems)|
|16:30||The cruise control system as a pilot application||Michael Jastram (University of Dusseldorf), Christine Rossa (Bosch), Rainer Gmehlich (Bosch)|
|17:00||The Rodin platform: latest and future additions||Michael Butler (University of Southampton)|
Event-B in Space – or are we still on the ground?
- Presenter : Dubravka Ilic, Space Systems Finland
- Description : The presentation will give a summary of the experience SSF gained while using Event-B, starting from choosing the right area for the application up to development trials with different refinement strategies. We will also address questions such as: what is still lacking in our models/in the tool/in the method, what are the known challenges so far, how do we expect to see commercial deployment of Event-B in space applications etc.
Formal Development of Enterprise Service Communication
- Presenter : Andreas Roth, SAP AG
- Description : This talk presents the pilot deployment in the sector of business information systems which takes place within the Deploy project. Special emphasis in this deployment is put on the integration of formal modeling with existing domain-specific modeling languages in the business information domain. As first result we describe the integration of Event-B with service choreography models.
- Presenter : Marc Benveniste, STMicroelectronics
- Description : The stepwise formal development of safety critical software is now a well established engineering practice, noticeably in railway systems. However, it has not been applied as successfully to hardware development, where formal methods are mainly used for verification and gate level transformations and optimizations. In this paper, we report our recent experience in the stepwise formal development of a real digital macro-cell, that opens the way to the design of digital circuits with zero functional bugs. We highlight the main design steps that can be followed to achieve the development of code ready to enter the synthesis flow. We start with a very simple model with few events, an abstraction of the macro-cell. Each step in the formal design flow is done using basic mathematics like sets theory and first order logic, as these are the B technology underpinnings. Its supporting free tool, Atelier B, is used for the proof work. The last step uses the B4SYN prototype translator to produce the source code that enters our standard synthesis flow. Finally, we provide some early comparison between the obtained code and the code for the same macro-cell developed in a traditional flow. This work has been done in the frame of the PACA Regional Council ST-focused project “FORmal CO-developMENT”, PS-17bis, in a close and fruitful collaboration with CLEARSY System Engineering.
- Presenter : Aryldo G Russo Jr. / AeS Group & Research Institute of State of Sao Paulo (IPT)
- Description : The use of formal methods has been growing constantly, but with basically two constraints: most of is usage is concentrated in Europe, its Mother land, and it’s been used only by big companies whom, some how, develops some kind of safety critical applications. In this paper, I try to present the usage stage of formal methods in other parts of the world, mainly South America. I will present some achievements that has been done so far. Besides previous work on formal methods, I will also present the modality of DEPLOY project, called DEPLOY Associate, and the project that AeS will be conducting based on this modality.
Probabilities in event-B for railways safety critical systems
- Presenter : Jérôme Falampin (Siemens Transportation Systems)
- Description : B and event-B are well adapted to demonstrate that a (safety, reliability…) property always hold, or that a (dangerous, unwanted…) state is never reached. But in real-life-systems, it may be acceptable that safety properties are violated providing that such situations are « rare enough ». A light (and yet incomplete) approach of probability within event B will be presented to model such requirement.
ProB for Validating Large Scale Railway Models
- Presenter : Michael Leuschel (University of Düsseldorf)
- Description : We present details about using ProB to validate various aspects of formal railway models. Notably, we describe recent improvements to be able to deal with large sets and relations, as well as various other improvements related to inspecting the truth value of complicated formulas. We also discuss progress on validating ProB itself so that it can be used within a SIL-4 development process.
Event B recipes for proof-based design of distributed systems
- Presenter : Dominique Méry, Université Henri Poincaré Nancy 1, LORIA, France.
- Description : The presentation will give a summary of works on Event B for dealing with distributed algorithms/systems and for providing guidelines for developing models. A collection of proof-based patterns are under investigation in the project RIMEL supported by ANR and lead to both case studies and systematic guidelines for improving the use of Event B. Partners of the project are CLEARSY and the LABRI laboratory.
The cruise control system as a pilot application
- Presenter : Michael Jastram (University of Dusseldorf) – Christine Rossa (Bosch) – Rainer Gmehlich (Bosch)
- Description : In DEPLOY, the formal specification method event-B is applied to automotive industrial problems, and in particular, to a cruise control system. To date, our most important assignment has been to develop a well-structured requirements document, leading the modeling of the cruise constrol system in event B. Several challenges have been identified that need to be addressed in the coming years.
- Presenter : Thierry Lecomte (CLEARSY)
- Description : Automatic refinement and code generation have been successfully applied in a number of industrial applications during the past 15 years. This talk presents some of these applications, where code generation addresses both hardware and software, and where safety and security are of paramount importance. This presentation is sided by several demonstrations of automatic refinement of software and code generation in C, Ada, Ladder and VHDL.
Formal Modeling Feedback on Train Tracking
- Presenter : Mathieu Clabaut (Systerel)
- Description : The presentation will give a summary of the experience Systerel gained while using Event-B to model a Train Tracking system. The modeling strategies, parts of the model and some open questions will be exposed.
- Presenter : Michael Butler (University of Southampton)
- Description : The Rodin platform is being extended within the framework of the DEPLOY project. This talk gives a clear picture of the current status of the tools and future work (roadmap). This presentation is sided by a demonstration of the recent additions.
L’accès à ce workshop est gratuit. L’inscription est toutefois obligatoire. Merci de se rendre sur la page suivante : S’enregistrer. Pour ce workshop, nous prévoyons d’accueillir une cinquantaine de personnes.