The Dyade/FormalFame Action (1998-2001)

followed by

The Bull-Inria "FormalFame" Project (2001-2004)

followed by

The Bull-Inria "FormalFame +" Project (2004-2007)

Version 1.54 - Date 2015/09/18 15:58:38


1. Overview

Initiated in 1999, FormalFame aims at applying formal methods and tools developed at INRIA in order to improve the quality and productivity of complex system designs.

The target of FormalFame is Fame, a multiprocessor architecture developed by Bull based on Intel's 64-bit Itanium-2 processors. The Fame architecture is used in Bull's NovaScale high-end servers.

FormalFame can be seen as the continuation of a previous project, the Dyade/Vasy action (1995-1998), in which formal methods and tools developed at INRIA were applied to the design of the PolyKid multiprocessor architecture developed at Bull.

Between 1998 and 2001, FormalFame took place in the framework of Dyade, a joint venture between Bull and Inria for advanced research. Since 2001, FormalFame is a collaboration project between Bull and the Vasy team of Inria.

The FormalFame project emcompasses several working areas:

The benefits of the approach used in the FormalFame project are the following:

Although there is an extra cost during the design phase (due to formal specification and verification), this cost is considered as a quality insurance cost.

Between 1998 and 2004, the collaboration focused on Fame, the Cc-Numa multiprocessor architecture used in Bull's NovaScale series of high-performance servers based on Intel Itanium processors. The CADP tools have been used to validate a crucial circuit of Fame — the Fss (Fame Scalability Switch) — that implements the cache coherency protocol. The technology transfer is complete, in the sense that the CADP tools are now part of Bull's validation methodology and that Bull maintains itself the Lotos specifications developed for Fame.

In 2004, the collaboration was renewed by a followup contract named FormalFame Plus, which, in 2005, was extended for two more years. The general goal of FormalFame Plus was to enhance the performance and usability of the CADP tools in prevision of the next multiprocessor architectures under design at Bull.

In 2007, the FormalFame Plus collaboration completed and found a direct continuation into the Multival project (pôle de compétitivité mondial Minalogic).

2. The Dyade/FormalFame Action - The "FormalFame" Project

Starting date: September 1998 (officially created in 1999)

Ending date: March 2004

Client within Bull: Bull Servers, Les-Clayes-sous-Bois (France)

INRIA hosting projects: Vasy (INRIA Rhône-Alpes), Pampa [1998-April 2000] (INRIA Rennes)

Operational supervision: Anne Kaszynski (Bull) [1998-March 2002], Sylvie Lesmanne (Bull) [since March 2002]

Scientific supervision: Hubert Garavel (INRIA Rhône-Alpes) [ongoing] and César Viho (INRIA Rennes) [1998-April 2000]

Technology transfer: Massimo Zendri (Bull) [1998-April 2000], Nicolas Zuanon (Bull) [May 2000-April 2001], Solofo Ramangalahy [June 2001-May 2004]

Team Members: Jacques Abily (Bull)
Damien Bergamini (INRIA Rhône-Alpes)
Marc Herbert (INRIA Rhône-Alpes)
Hubert Garavel (INRIA Rhône-Alpes)
Claude Jard (INRIA Rennes)
Thierry Jéron (INRIA Rennes)
Anne Kaszynski (Bull)
Sylvie Lesmanne (Bull)
Radu Mateescu (INRIA Rhône-Alpes)
Bruno Ondet (INRIA Rhône-Alpes)
Frédéric Perret (INRIA Rhône-Alpes)
Solofo Ramangalahy (INRIA Rennes, then Bull)
Séverine Simon (INRIA Rennes)
César Viho (INRIA Rennes)
Yehong Xing (Bull)
Massimo Zendri (Bull)
Nicolas Zuanon (Bull)

3. The "FormalFame Plus" Project

Starting date: April 2004

Ending date: March 2007

Client within Bull: Bull Servers, Les-Clayes-sous-Bois (France)

INRIA hosting projects: Vasy (INRIA Rhône-Alpes)

Operational supervision: Sylvie Lesmanne (Bull)

Scientific supervision: Hubert Garavel (INRIA Rhône-Alpes)

Team Members: Azedine Abdelli (Bull)
Jacques Abily (Bull)
Damien Bergamini (INRIA Rhône-Alpes)
David Champelovier (INRIA Rhône-Alpes)
Hubert Garavel (INRIA Rhône-Alpes)
Frédéric Lang (research scientist)
Sylvie Lesmanne (Bull)
Radu Mateescu (INRIA Rhône-Alpes)
Wendelin Serwe (INRIA Rhône-Alpes)
Yehong Xing (Bull)

4. Publications

Prior publications related to "PowerScale" and "Polykid"

To get an idea of the scientific approach used in FormalFame, you can read the four publications describing the work previously done in the Dyade/Vasy project.

Publications related to "FormalFame"

[5] SEQ.OPEN: A Tool for Efficient Trace-Based Verification
Hubert Garavel and Radu Mateescu
in Proceedings of the 11th International Workshop on Model Checking of Software SPIN'2004, Barcelona, Spain, April 2004.

[6] Almost Ten Years of Process Algebras and Model Checking for Multiprocessor Architectures slides by H. Garavel (joint work with many other persons at Bull and INRIA), May 2004.

5. Yearly Activity Reports

See also the yearly activity reports of the INRIA/VASY team, available from the Press Releases Page, and especially:

See also:

6. About Fame and NovaScale

Official information available from Bull's Web sites:

Back to the VASY Home Page