Bull
INRIA

FormalFame Plus 2007 Activity Report

Contents

Introduction

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

Team

BULL Jack Abily
Ghassan Chehaibar
Sylvie Lesmanne (project leader)
Yehong Xing
Meriem Zidouni
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 2007, 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 2007, we performed maintenance activities for these tools, fixing a few errors. We also modified in many places the C code generated by Csar and Csar.adt to avoid all warnings emitted by recent C compilers with the strictest code-checking options. For the end-user, this eases the development of Lotos specifications by guaranteeing that all warnings seen when compiling the C code generated by Csar and Csar.adt are relevant to the source Lotos description (e.g., unused parameters of some Lotos operation) or to the hand-written C code provided by the user (and are not meaningless warnings arising from C code generation artefacts).

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. We improved the results of our reduction technique based on live variable analysis by allowing data-flow optimizations to be repeatedly applied in a hierarchical manner on parts of the Lotos specification. On 151 out of 684 benchmarks, we observed a reduction in the numbers of states (by a mean factor of 2.49 and a maximum factor of 24.27) and of transitions (by a mean factor of 2.41 and a maximum factor of 23.54).

Compilation of Lotos NT

We continued to improve the Lnt2Lotos tool suite that translates (a large subset of) Lotos NT into Lotos, thus allowing to use Cadp to verify Lotos NT descriptions. Bull is using this tool suite to model and verify critical parts of its Fame2 multiprocessor architecture.

In 2007, we brought the following improvements:

Lnt2Lotos is developed using the Syntax/Traian technology. Currently, it represents 22,300 lines of code (3,700 lines of Syntax code, 16,500 lines of Lotos NT code, and 2,200 lines of C code). The Lotos NT reference manual was updated and grew from 47 pages (at the end of 2006) to 61 pages.


Go back Back to the VASY Home Page