Section: Overall Objectives

History

The project Formes was created by union of three different smaller groups, the origin and interests of which were somewhat different: a group working on simulation of embedded systems at CASIA since march 2007 under the leadership of Vania Joloboff; a second group working on user-assisted theorem proving under the leadership of Jean-Pierre Jouannaud originated from the Inria project-teams LogiCal at Inria-Saclay-Île-de-France and Protheo at Inria-Lorraine; and a group working on model-checking and trustworthy computing at Tsinghua University under the leadership of Gu Ming. The second group moved from France to Beijing in September 2008. A previous 4 weeks visit of Jean-Pierre Jouannaud and Frédéric Blanqui in March 2008 had been used to define the new project Formes , and prepare its installation at Tsinghua university.

Formes is the acronym for FORmal Methods for Embedded Systems, and indeed we aim at combining in this project formal methods of very different origins for analyzing embedded systems. We develop a software SimSoC for simulating embedded systems, but we also develop other techniques and tools in order to analyze and predict their behavior, and that of the software running on such systems. These techniques themselves are of different origin, and are usually developed in different teams around the world. Verification techniques based on model checking have been extensively and successfully used in the past to analyze hardware systems. Decisions procedures, like SAT, are now common place to analyze specific software applications, such as scheduling. Proof assistants are more and more employed to carry out formal proofs of correctness of security protocols and more generally non-trivial pieces of software. One originality of our project is to combine all these techniques in order to achieve our goal: to design methods and tools allowing one to build reliable software, also called trustworthy computing. In the next sections, we describe in more details these five areas, and their relationship to Formes .