FormalFame Plus 2007 Activity Report

Contents

• Introduction
• Team
• Progress report

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

Progress report

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

• We continued the development of our Lnt2Lotos tool suite, which was used by Bull.
• We experimented various abstraction and verification techniques on a critical part of Bull's Fame2 multiprocessor architecture.

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 2007, we performed maintenance activities for these tools, fixing a few errors. We also modified in many places the C code generated by Cæsar and Cæsar.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 Cæsar and Cæsar.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 Cæsar, 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:

• As regards the data part of Lotos NT, a new type constructor "array [n..m] of T" was added to Lotos NT at Bull's request and implemented in the tool suite.

• As regards the process part of Lotos NT, we finalized the definition of processes and behaviors, ensuring language symmetry in the sense that most Lotos NT constructs used in functions are also allowed in processes (absence of such a nice symmetry is a drawback of Lotos making the language harder to learn). The concrete syntax and static semantics of processes have been specified. The translation of Lotos NT process definitions is under development.

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.

Back to the VASY Home Page