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)
Frédéric 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 Cæsar.adt compiler for the data type part of Lotos, the Cæsar compiler for the process part of Lotos, and the Cæsar.Indent pretty-printer.

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