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.
| 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) |
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:
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:
We simplified the use of the Exec/Cæsar environment. Exec/Cæsar allows to interconnect, on the one hand, the C code generated by Cæsar from the Lotos description of a system and, on the other hand, the ``real'' environment with which this system interacts. This interconnection is implemented as a collection of C functions, one per visible gate declared in the Lotos specification, which have to be written by hand.
The new version of Cæsar greatly automates this task by generating automatically, for each function, a C code skeleton that implements appropriate pattern-matching actions for checking gate parameters — since, in Lotos, the same gate can be overloaded with several parameter lists that differ in number, types and direction (input or output) — as well as logging actions to trace the execution of these functions.
We pursued our study of state space reduction techniques, our goal being to decrease the size of the graphs generated by Cæsar, still preserving strong bisimulation between the original and reduced graphs.
Our previous work on state space reduction based on live variable analysis led to an improved version of Cæsar (named Cæsar.New), which became part of Cadp in April 2005. A journal paper was also accepted for publication.
Additionally, W. Serwe experimented further uses of data-flow analysis so as to reduce memory requirements for enumerative verification.
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.
Back to the VASY Home Page