The Formose consortium is composed of two academic partners (IMT and LACL) and three companies (ClearSy, OpenFlexo, THALES). All the partners share a strong background in formal methods.
Formose ANR Project
Formal Requirements Modeling for Critical Complex Systems, Method and Toolkit
ClearSy
ClearSy System Engineering is specialized in safety critical and safety systems, where all activities (specification, design, development, testing, validation, auditing) are based on the B formal method. With the support from RATP, SNCF, INRETS, French Government and the EU, ClearSy has developed a number of tools (Atelier B, B Automatic Refinement Tool, Brama model animator). Since 1994 ClearSy has been in charge of dissemination of the B technology and methodology. ClearSy is now actively deploying them in industry (railways, microelectronics, information systems, defense, automotive). Its main activity now concerns the development of secure and safety critical systems with B, mainly based on PLCs (over speed radar, platform screen-doors control/command, train passage detector, etc.).
LACL
The LACL-University Paris Est Créteil laboratory (Laboratoire d’Algorithmique, Complexité et Logique) gathers about 50 members, professors, assistant professors, PhD students and postdocs. It focuses on two topics: on one hand, Logic, Computation and Programming and, on the other hand, Specification and Verification of Systems.
OpenFlexo
OpenFlexo is an OpenSource project aiming at building a generic platform for multifaceted modeling and artefact generation (like document and code generation). It is evolving from a mature modeling workbench targeted at Business Process Modeling, toward a full-featured infrastructure supporting multi-paradigm and viewpoint modeling.
Telecom Bretagne
The Institut Mines-Telecom is a group of "Grandes Ecoles" (prestigious French higher education establishments) in the field of information and communication technology (ICT). Two schools of the Institut Mines-Telecom are involved in the project. The first one is Télécom Bretagne. Member of IRISA, the PASS team, located in Brest, gathers lecturers of the computer science department of Télécom Bretagne. The team aims at studying design processes, product models and their relationships.
Telecom SudParis
The Computer Science Department of Télécom SudParis (UMR Lab-SAMOVAR 5157) is doing research in different domains related to the modeling and the verification of critical systems such as transportation. To this aim, various verification techniques, including proof, test and model checking, are used to check a large range of properties from static to dynamic properties by including timed aspects.
THALES
THALES is a world leader for mission critical information systems: aerospace & space, defense, security. THALES designs and provides global solutions of airspace security for civil domain. In civil avionics, THALES develops traffic management systems, tools to provide assistance during the landing phase, for the navigation and to secure airport areas. In this domain, THALES proposes a full set of surface radars.
