The Dyade/FormalFame Action

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.56 - Date 2021/02/09 19:26:18

1. Overview
2. The Dyade/FormalFame Action - The "FormalFame" Project
3. The "FormalFame Plus" Project
4. Publications
5. Yearly Activity Reports
6. About Fame and NovaScale

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:

Formal specification
The formal specification task consists in producing a mathematical, unambiguous model of the complex architecture/protocol under study. The modeling is done at an abstract level that hides the irrelevant implementation details. The specification language used is LOTOS (ISO standard 8807). Formal specification often allows to clarify ambiguities and to detect design errors at the very beginning of the development process.
Rapid prototyping
The formal specification can be used as a basis to generate executable code using a LOTOS compiler. The generated code serves for simulation and emulation purpose. This allows to perform further debugging of the design, taking advantage of the available formal specification. The toolset used for compiling LOTOS programs is CADP (Construction and Analysis of Distributed Processes).
Model-checking verification
Simulation and emulation allow some debugging of the formal specification, but do not give a total confidence in the correctness of the design. Using model-checking techniques, it is possible to verify critical requirements on down-sized configurations exhaustively, while the traditional tests and simulations are used to perform non-exhaustive verification on larger configurations. The toolset used for verification is CADP.
Automatic test generation
It consists in generating test cases from a formal specification and formal test purposes. This approach cuts the costs of test activity: the automatically generated test cases send inputs to the implementation and check that the implementation's outputs are correct with respect to the formal specification. This avoids the manual writing of all the interactions of a test case and the development of a test checker; by doing so, more complex tests and a better test coverage can be obtained.

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

Master the design complexity for high-end multiprocessor architectures
Improve the productivity during the design phase
Increase confidence in the design
Clarify issues and detect errors in the earlier phases of the development process
Decrease the implementation cost, as most errors have been detected before implementation
Decrease the testing cost, as test cases are automatically generated
Decrease the maintenance cost, as the design is formally documented
Improve the quality of the final product
Reduce the risk of delays

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.