LCHIP project (Low Cost High Integrity Platform) will ease development of safety critical systems and software up to SIL4, the highest Safety Integrated Level. LCHIP platform is a combination of a B method (formal method) Integrated Development Environment and a secured runtime platform able to execute software in real-time.
Atelier B has turned 20
At the occasion of the ABZ 2016 conference (http://www.cdcc.faw.jku.at/ABZ2016/) which took place in Linz (Austria) on May 23-27 2016, ClearSy was invited to present the last 20 years of development and industrial use of Atelier B, and to expose forthcoming innovations including functional modelling (Abstract Model Editor), improved automatic proof and low-cost high-integrity platform (LCHIP). […]
Double-Core SIL4 Architecture Presented During Open Source Innovation Spring (Paris)
At the occasion of the seminar entitled “Languages and tools for Software Reliability” (May 12th 2016, Jussieu (Paris)) that will take place during the Open Source Innovation Spring, ClearSy will present the Double-Core SIL4 architecture aimed at low-cost safety critical automation. This architecture relies on innovative safety principles and a software development formal tool-chain. Software […]
Atelier B 4.3.1 is Available for Maintenance Holders
We are pleased to inform you that Atelier B 4.3.1 is available for download. It is exclusively reserved for maintenance holders, and is accessible from the account page (https://www.atelierb.eu/en/customer-account/ ) This version contains 27 fixes and two new features: a new prover based on the ProB tool and the B Coding Rule Checker. The integration […]
Formal Data Validation Tutorial at ABZ 2014, Toulouse
At the occasion of the ABZ 2014 conference, a tutorial on formal data validation is organized at ENSEEIHT together with workshops (see details here). The tutorial will happen on June 3rd 2014 from 2:00 pm to 5:30 pm. During this tutorial, formal data validation principles will be exposed (key concepts, mathematical language to express properties, […]
Atelier B 4.2.1 Free
Atelier B 4.2.1 Free is available for download. It corrects the errors related to the introduction of the new tool bxml and the lack of default values for the required resources.
Bxml errors with Atelier B 4.2 Free
New bxml tool included in atelier B 4.2 Free is not working properly as required resources are missing. When used, error messages “Bxml error for …” are displayed. The turnaround consists in adding the following lines: ATB*ATB*Proof_Obligations_Generator_NG_Command: pog ATB*ATB*Bxml_Command: bxml to the AtelierB file. A new version 4.2.1 is being cooked and should be available […]
ATELIER B 4.2 CELEBRATES 20 YEARS
Atelier B 4.2 Community Edition has been released on December 19, 2014. This release brings 151 bug corrections and 47 improvements. Among these features, we may mention: A new traceable, generic, proof obligation generator Addition of a proof server, in order to distribute and speed up proof A better integration of real and floating point numbers Full 64-bit […]
b2llvm: B developments onto the LLVM
David Deharbe – Universidade Federal do Rio Grande do Norte, Natal, Brazil Abstract: In this talk we describe a multi-platform code generator for the B method. In particular, we present a translation procedure from a larghe subset of the B language for implementations towards LLVM source code. This translation is defined formally as a set […]
Atelier B 4.1.1
Atelier B 4.1.1 is available for download for Atelier B 4 maintenance contract holders. This release brings 59 bug corrections and 7 improvements. Most corrections are related to unwanted man-machine behaviour: Atelier B: 41 bug corrections, 4 improvements Bart: 13 bug corrections, 3 improvements Code generators: 2 bug corrections Mathematical rules proof tool: 3 bug […]