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