CAI 2013 Conference

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.

Dagstuhl Seminar 2013

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 […]

SuperZenon to provide another prover to Atelier B

“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 […]

Formal verification of PLC programs using the B method

We pusblish this report which is related to safety critical industrial automation systems. Author: Haniel Moreira Barbosa Advisor: David Déharbe Date: October 2012 Nature: Submitted for the Graduate “Systems and Computer” Program Department of Computer Applied Mathematics and Informatics of the Federal University Rio Grande do Norte (Natal – Brazil).  Summary:  PLCs (acronym for Programmable Logic Controllers) […]

Technical conference on formal method organized by Aerospace Valley

The Aerospace Valley center (DAS embedded system), with the support of the ISFE theme of the RTRA AE/SE, organized a series of technical conferences on formal methods of development. Clearsy took part in the first conference on November 13th 2012 at the Aeronautic and Space Institute (IAS) in Toulouse, France. During the conference one of […]

Data Validation / Generation

Data validation and generation are of paramount importance in the railways, in order to ensure safety at the system level. Several studies/works have been conducted the past years: Verification  tool development, by RATP, initally based on PredicateB predicate calculus engine (part of Brama Event-B model animator), then completed by the ProB model-checker; data validation conducted by Siemens Transportation […]

BWare: a new project on proving B proof obligations

BWare, a  new research project related to the B method has started in September 2012. It is  funded for a period of 4 years by the programme “Ingénierie Numérique & Sécurité” of the French national agency ANR. This project is aimed at providing a mechanized framework to support the automated verification of proof obligations coming from the development of industrial […]

From Research to Teaching Formal Methods: the B Method

June 7th 2010, Nantes, France Presentation The workshop “From Research to Teaching Formal Methods: the B Method” was held in Nantes June 7, 2010, at “Journées Scientifiques de l’Université de Nantes”. This workshop was attended by thirty people, coming from France, Germany, Switzerland and Hungary. Various studies on B, Event-B and associated tools have been […]

Bibliography: Jean-Raymond Abrial publishes a book dedicated to Event-B

Jean-Raymond Abrial’s Event-B book has been published in may 2010. This 600+ page book, written in english, is entitled “Modeling in Event-B: System and Software Design”. It deals with system and software modeling in Event-B, a language issued from the B Method and allowing the description of systems with events.