FORMES Research team

Formal Methods for Embedded Systems

Team presentation

FORMES is one of the projects run within the LIAMA Consortium, as a cooperation project between INRIA, Tsinghua and Beihang Universities. This project is aiming at making research advances towards the development of safe and reliable embedded systems, by exploiting synergies between two different approaches, namely (real time) hardware simulation and formal proofs development.

Research themes

The FORMES team aims at addressing the challenges of embedded systems design with a new approach, combining fast hardware simulation techniques with advanced formal methods, in order to formally prove qualitative and quantitative properties of the final system. This approach requires the construction of a simulation environment and tools for the analysis of simulation outputs and proofs of properties of the simulated system. We therefore need to connect simulation tools with code-analyzers and easy-to-use theorem provers for achieving the following tasks:
  • Enhance the hardware simulation technologies with new techniques to improve simulation speed, and produce program representations that are adequate for formal analysis and proofs of the simulated programs;
  • Connect validation tools that can be used in conjunction with simulation outputs that can be exploited using formal methods;
  • Extend and improve the theorem proving technologies and tools to support the application to embedded software simulation.

International and industrial relations

  • The FORMES team is a project run in cooperation with the University of Tsinghua which hosts the project, Beijing University of Aeronautics and Astronautics and the University of Science and Technology at Beijing.
  • SIVES is a recently awarded project, with INRIA as leader on the French side, Tsinghua University on the Chinese side, and with the participation of Beihang university. SIVES is funded by ANR and the National Science Foundation of China.
  • The simulation part of the project is sponsored by Schneider Electric China.

Keywords: Formal methods Proof Coq Certification Embedded systems Simulation Compilation

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social