FormalFame Plus 2006 Activity Report

Contents

• Introduction
• Team
• Progress report

Introduction

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

Team

Progress report

In 2006, 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 2006, we performed maintenance activities for these tools (two bugs fixed in Cæsar, one bug fixed in the Cæsar.bdd tool invoked by Cæsar, and two enhancements in Cæsar.indent). We also improved the C code generated by Cæsar and Cæsar.adt to avoid warnings emitted by the most recent C compilers.

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 work on state space reduction based on live variable analysis resulted in version 7.0 of Cæsar (previously named Cæsar.new), which was officially released as part of Cadp in July 2006.

Additionally, W. Serwe experimented further uses of data-flow analysis to improve the efficiency for enumerative verification. A prototype version of Cæsar was developed and experimented in the framework of the FormalFame Plus contract: we obtained a memory reduction by a factor of 1.4 and a time reduction by a factor of 2.

Compilation of E-LOTOS

We continued the development of a tool suite for the translation from Lotos NT to Lotos, which aims at easing the development of large specifications by Bull and to reuse the existing Lotos tools for analyzing concurrent systems described in Lotos NT. The tool suite consists of a Lotos/Lotos NT preprocessing tool named Lpp, a translator from Lotos NT data types to Lotos named Lnt2Lotos, and a shell script named Lnt_Compile, which calls Lpp and Lnt2Lotos.

In 2006, the tool suite was improved as follows:

• The predefined comparison functions (``='', ``<'', ``≤'', etc.), which were only available for enumerated types in 2005, were made available to all constructor types, using a recursive lexicographic ordering of constructors and constructor fields.

• A new predefined type ``sorted list of T'' was added. The elements of a sorted list are sorted automatically using the order relation ``<'' on T, which can be either generated automatically as explained in the previous item, or given by the user.

• We implemented the translation from Lotos NT functions into Lotos equations, starting from an algorithm that translates into Horn clauses a subset of the C language (``while'' loops without ``break'' statements and functions with value passing parameters only and a single ``return'' statement located at the end of the function). We extended this algorithm so as to handle reference passing parameters, pattern matching (``case'' statement), loop interruptions (``break'' statement), multiple ``return'' statements within the body of functions, uncatchable exceptions (``raise'' statement), and function name overloading.

• The Lnt_Compile tool was improved to allow the generated Lotos code to be combined with handwritten Lotos code and/or C code provided by the user.

Lnt2Lotos is developed using the Syntax / Traian technology. It grew from 3, 660 lines (760 lines of Syntax code, 1, 920 lines of Lotos NT code, and 980 lines of C code) at the end of 2005 up to 17, 300 lines (2, 100 lines of Syntax code, 14, 000 lines of Lotos NT code, and 1, 200 lines of C code) at the end of 2006.

In 2006, we delivered 7 successive versions of the tool suite to Bull, who uses Lotos NT to model a critical part of its Fame2 multiprocessor architecture for high-end servers. A non-regression test suite of 67 programs representing more than 6, 000 lines of Lotos NT code was developed. The reference manual was updated and grew from 29 pages (at the end of 2005) up to 47 pages (at the end of 2006). A forge was set up under Inria GForge to track bugs and feature requests, and to serve as a repository where our Bull partners can download the new versions of the Lnt2Lotos tool suite.

Back to the VASY Home Page