Bull
INRIA

FormalFame Plus 2005 Activity Report

Contents

Introduction

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

Team

BULL Jack Abily
Sylvie Lesmanne (project leader)
Yehong Xing
INRIA / VASY Damien Bergamini (software engineer, until January 30th, 2005)
David Champelovier (software engineer, since May 1st, 2005)
Hubert Garavel (research director)
Frdric Lang (research scientist)
Radu Mateescu (research scientist)
Wendelin Serwe (research scientist)

Progress report

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

In 2005, the contributions of Vasy 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 2005, we performed maintenance activities for the tools (1 bug fixed in Csar.adt, 1 bug fixed in Csar, and 3 bugs fixed in Csar.Indent) and we improved the C code generated by Csar and Csar.adt to avoid warnings emitted by the most recent C compilers. We also enhanced the Csar compiler in two ways:

Compilation of E-LOTOS

We undertook the definition of an automatic translator from Lotos NT to Lotos. This will allow Bull to develop formal models in a faster way, as Lotos NT is more concise than Lotos and closer to mainstream programming languages.

In 2005, a first version of this translator was delivered to Bull. It consists of a Lotos preprocessing tool named Lpp (1, 280 lines of C code) and a translation tool named Lnt2Lotos developed using the aforementioned Syntax/Traian technology (760 lines of Syntax code, 1, 920 lines of Lotos NT code, and 980 lines of C code). A reference manual was written.


Go back Back to the VASY Home Page