Software Design and Validation by the LANDE Research Group at Inria-Rennes
by Daniel Le Métayer
The LANDE research group at IRISA Rennes (a joint laboratory of INRIA,
CNRS, University of Rennes and INSA) designs tools for the development
and the validation of software. These tools rely on firm theoretical foundations
and are as mechanical as possible in order to be acceptable for users who
are not experts in formal methods. The project involves about 20 people,
including 10 PhD students.
We distinguish two kinds of contributions, which tackle the problem
at two different levels. The first concerns the program development phase:
examples of our contributions in this category include a new formalism
for the description of software architectures and a richer type system
for the C language. The second concerns the validation of existing code
(verification, testing). Our work on this topic is related to fundamental
aspects of static analysis as well as the design of specific analyses,
for instance for program debugging or for the verification of security
properties, and the conception of debugging and test case generation tools.
Specification of Software Architecture Styles based on Graph Grammars
We have proposed a definition of software architectures in terms of
graphs, which constitute the mathematical model closest to the intuition
conveyed by the 'box and line' drawings traditionally used by software
designers. An architecture style is a class (or set) of architectures exhibiting
a common shape. Technically, architecture styles are defined as context-free
graph grammars. The architecture can be seen as the skeleton of an application.
In order to be executable, it must be 'fleshed out', or completed with
a mapping from nodes to entities defined in a given language. Our approach
makes it possible to reconcile a dynamic view of the architecture, which
is crucial for a large class of applications, with the possibility of static
checking, ensuring that the evolution of the architecture conforms to its
style. This verification can be seen as a form of static type checking
of the architecture transformer. Our work on software architectures is
done within the European working group Coordina.
A Type System for the Safe Manipulation of Pointer Data Structures
The type systems currently available for imperative languages are too
weak to detect a significant class of programming errors. For example,
they cannot express the property that a list is doubly-linked or circular.
Our solution to this problem is based on a notion of shape types defined
as context-free graph grammars. Graphs are defined in set-theoretical terms,
and graph modifications as multiset rewrite rules. These rules can be checked
statically to ensure that they preserve the structure of the graph specified
by the grammar. We have provided a syntax for a smooth integration of shape
types in C. The programmer can still express pointer manipulations with
the expected constant time execution and benefits from the additional guarantee
that the property specified by the shape type is an invariant of the program.
Formalisation of Security Policies for Java
Security is one of the most important issues concerning the Java language,
at least in the context of its application to the programming of mobile
code. Furthermore, Java includes a unique combination of features which
makes the study of security issues especially challenging. In particular,
the visibility rules of the language and the class loading mechanism have
a strong impact on security. We have proposed a formalisation of these
aspects of the language which is at the right level of abstraction to support
reasoning on security properties. We are currently extending this formalisation
to be able to specify security policies and study the constraints that
they impose on various components such as the class loader or the security
manager. This work is done within the action VIP of DYADE (which is a Bull-Inria
joint venture).
Generic Slicing Analysis Based on a Natural Semantics Format
Dynamic and static slicing analyses have been proposed for different
programming languages. Rather than defining a new analysis from scratch
for each programming language, we would like to specify such an analysis
once for all, in a language-independent way, and then specialise it for
different programming languages. In order to achieve this goal, we have
proposed a notion of natural semantics format and a dynamic slicing analysis
format. The natural semantics format formalises a class of natural semantics
and the analysis format is a generic, language-independent, slicing analysis.
The correctness of the generic analysis is established as a relation between
the derivation trees of the original program and the slice. We have shown
that it is possible to get slicing analyses for various programming languages
(imperative, functional, logic) by mere instantiation of the generic analysis.
Automated Debugging by Trace Analysis
We have defined a general trace query language which is based on a model
of programs expressed in terms of streams of events. The user can express
queries about the execution traces in a logic programming style. Queries
can be evaluated on the fly or off line. The first option makes it possible
to analyse very long traces and the second one can be applied after the
execution of the program. We have defined in this language analyses providing
abstract views of the execution (according to criteria like control flow
or data flow). An important feature of the approach is that it is not tied
to one specific programming language. We are currently using it for the
development of a debugging tool for the Mercury language. This work is
done within the European R&D project Argo (with Mission Critical (Belgium),
Dassault Electronique (France), the university of Melbourne (Australia)
and the Facultés Universitaires Notre Dame de la Paix of Namur (Belgium).
Casting: A Formally Based Software Test Generation Method
We have designed Casting (Computer Assisted Testing), a tool which is
able to generate realistic software test suites in a formal and semi-automatic
way. Based on a two-layer modular architecture, Casting is not tied to
any particular style of input. It supports functional testing as well as
structural testing and offers a rich interface to the user, including the
specification of testing strategies. Two layers are distinguished in Casting:
the administrator layer, which provides configuration features (syntax
of the input language and basic extraction rules and strategies), and the
user layer, which assists test designers in generating test suites from
a given input text. Before starting their effective generation, the system
provides an estimation of the number of test cases. This estimation can
be used interactively to adjust the strategy in order to produce an acceptable
number of test cases. The generation involves a constraint solving phase.
A significant feature of Casting is that it generates test suites (sequences
of calls to the system's operations) rather than test cases, which makes
it possible to provide its output directly to the software under test (after
translation into the implementation language). Casting is developed in
collaboration with AQL (Alliance Qualité Logiciel), a french software
company located in Rennes.
For more information, see: http://www.irisa.fr/EXTERNE/projet/lande/Lande_anglais.html
Please contact:
Daniel Le Métayer
Tel: +33 2 99 84 73 06
E-mail: lemetayer@irisa.fr
