Bull
INRIA

FormalFame Plus 2006 Activity Report

Contents

Introduction

This page is an excerpt from the VASY project activity report for year 2006. It is composed of the parts that concern the FormalFame Plus contract.

Team

BULL Azedine Abdelli
Jack Abily
Sylvie Lesmanne (project leader)
Yehong Xing
INRIA / VASY David Champelovier (software engineer)
Hubert Garavel (research director)
Frdric Lang (research scientist)
Radu Mateescu (research scientist)
Wendelin Serwe (research scientist)

Progress report

In 2006, the contributions of Vasy to FormalFame Plus were the following:

Compilation of LOTOS

The Cadp toolbox contains several tools dedicated to the Lotos language, namely: the Csar.adt compiler for the data type part of Lotos, the Csar compiler for the process part of Lotos, and the Csar.Indent pretty-printer.

In 2006, we performed maintenance activities for these tools (two bugs fixed in Csar, one bug fixed in the Csar.bdd tool invoked by Csar, and two enhancements in Csar.indent). We also improved the C code generated by Csar and Csar.adt to avoid warnings emitted by the most recent C compilers.

We pursued our study of state space reduction techniques, our goal being to decrease the size of the graphs generated by Csar, still preserving strong bisimulation between the original and reduced graphs.

Our work on state space reduction based on live variable analysis resulted in version 7.0 of Csar (previously named Csar.new), which was officially released as part of Cadp in July 2006.

Additionally, W. Serwe experimented further uses of data-flow analysis to improve the efficiency for enumerative verification. A prototype version of Csar was developed and experimented in the framework of the FormalFame Plus contract: we obtained a memory reduction by a factor of 1.4 and a time reduction by a factor of 2.

Compilation of E-LOTOS

We continued the development of a tool suite for the translation from Lotos NT to Lotos, which aims at easing the development of large specifications by Bull and to reuse the existing Lotos tools for analyzing concurrent systems described in Lotos NT. The tool suite consists of a Lotos/Lotos NT preprocessing tool named Lpp, a translator from Lotos NT data types to Lotos named Lnt2Lotos, and a shell script named Lnt_Compile, which calls Lpp and Lnt2Lotos.

In 2006, the tool suite was improved as follows:

Lnt2Lotos is developed using the Syntax / Traian technology. It grew from 3, 660 lines (760 lines of Syntax code, 1, 920 lines of Lotos NT code, and 980 lines of C code) at the end of 2005 up to 17, 300 lines (2, 100 lines of Syntax code, 14, 000 lines of Lotos NT code, and 1, 200 lines of C code) at the end of 2006.

In 2006, we delivered 7 successive versions of the tool suite to Bull, who uses Lotos NT to model a critical part of its Fame2 multiprocessor architecture for high-end servers. A non-regression test suite of 67 programs representing more than 6, 000 lines of Lotos NT code was developed. The reference manual was updated and grew from 29 pages (at the end of 2005) up to 47 pages (at the end of 2006). A forge was set up under Inria GForge to track bugs and feature requests, and to serve as a repository where our Bull partners can download the new versions of the Lnt2Lotos tool suite.


Go back Back to the VASY Home Page