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