Proven software with B executing on Low Cost High integrity Platform”, is aimed at presenting the latest innovations concerning the use of the B formal method for the development of safety critical systems
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 […]
ABZ 2014 conference was held from June 2d to 6th in Toulouse. It was attended by about 120 people and allowed B, Z, ASM, Alloy and VDM communities to meet and exchange ideas. The diversity and relevance of the work presented, as well as the presence of significant industrial, reflect a growing force in the […]
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, […]
On March 14th, 2014, we shall present to M2 STL students – Pierre & Marie Curie University in Paris, various industrial cases of the use of the formal B method.
ClearSy is contributing to a technical seminar organized by Newcastle University on 24 October 2013. Formal methods are used worldwide to improve safety in several railways applications, at various levels and with a wide range of results obtained. This presentation is intended to provide a unified (not agnostic) overview of existing practices and to assess to which […]
ClearSy participated to CAI 2013 conference (International Conference on Algebraic Informatics) held in Porquerolles (France) 3-6 September 2013. A talk, entitled “Railways formal data validation“, was given during the industrial session.
ClearSy attended a Seminar,”Integration of Tools for Rigorous Software Construction and Analysis” (13372), held at Schloss Dagstuhl in Germany (8-13 September 2013). The program spans from theoretical and methodological foundations to practical applications, emphasizing system engineering methods and tools that are distinguished by their mathematical rigor and have proved to be industrially viable. A main goal of the […]
System level proofs for the CBTC of the New York Flushing line has been presented on June 26th 2013 in Paris. The aim of this presentation is to give the participants an insight of what has been done in this system level proved, what methods have been used, and what are the results and their practical usage.
“SuperZenon is an experimental extension of the Zenon automated theorem prover, using the principles of superdeduction, among which the theory is used to enrich the deduction system with new deduction rules. Superdeduction is a variant of deduction modulo, which is an extension of logical deduction systems consisting in canonically adding ad hoc deduction rules translating […]