Project
Presentation
The Lande project is concerned with formal methods
for constructing and validating software. Faced with the complexity of
modern software, we have adopted an approach in which a given piece of
software is described by views where each view provides a partial
description of the organisation or the behaviour of the software. The
difficulty with this approach when used in software construction is
that multi-view specification must be verified for coherence in order
to assure that two views do not contradict each other.
Furthermore, view-based validation of software requires sophisticated
analysis techniques for extracting precise partial information about a
piece of software in a cost-effective way. Our focus is on providing
methods with a solid formal basis (in the form of a precise semantics
for the programming language used and a formal logic for specifying the
views) in order to provide firm guarantees as to
their correctness. In addition, it is important that the methods
provided are highly automated in order for them to usable by
non-experts in formal methods.
The Lande project is a joint project with the CNRS,
the University of Rennes 1 and Insa Rennes.
Research themes
The goal of multi-view descriptions of software
architectures is to specify the organisation of large software systems
in a way that facilitates their development (specification, analysis,
implementation, test and maintenance). In particular, it is hoped that
this approach will allow techniques such as program analysis,
refinement and refinement to scale. Our activity is primarily concerned
with guaranteeing coherence between different views. The main challenge
here is to find the proper mathematical notions for relating views
representing properties of different kind an level of abstraction. Once
such a relation has been established, coherence can be checked by means
of standard techniques from static analysis and verification.
The new programming paradigm called aspect-oriented
programming consists in expressing a program as a central component
together with a collection of views or aspects that describe particular
tasks such as memory management, synchronisation, optimisation etc.
that the program must implement. A tool, called a weaver, is then
supposed to integrate these views with the main component
producing the final program. The benefit of this approach is locality:
implementation choices are centralised (in an aspect) rather than being
scattered all over the program. After having used aspect-oriented
programming for securing mobile code, we are now studying the problem
arising from interaction between aspects. As with the multi-view
specifications, aspects are not always orthogonal, and conflicts or
ambiguities may arise during program weaving. A more recent activity
concerns an aspect-oriented language for component composition.
We have defined a framework for studying logical
information systems in which activities such as navigation, querying
and data analysis can be studied at the same level. This framework
presents the advantage of being generic in the logic used for
navigation and querying; in particular it can be instantiated with
different types of program logics such as types or other static
properties. This facilitates the navigation and organisation of large
software systems.
Our activity in the area of programming language
security has lead to the definition of a framework for defining and
verifying security properties. Our approach is based on a combination
of static program analysis and model checking. This framework has been
instantiated to the specification and validation
of security policies for applications written in the Java 2 security
architecture and for the verification of security properties of
multi-application smart cards programmed using the Java Card language.
In terms of static program analysis we have conducted
research on the foundations and the implementation of static program
analyses as well as on particular analyses such as pointer analysis for
C and control flow analysis for Java and Java Card. Our foundational
studies concern the specification of analyses by inference systems and
the classification of analyses with respect to precision using abstract
interpretation. For the implementation of analyses, we are improving
and analysing existing iterative techniques based on constraint-solving
and rewriting of tree automata.
In order to facilitate the dynamic analysis of
programs we have developed a tool for manipulating execution traces.
The distinctive feature of this tool is that it allows the user to
examine the trace by writing queries in a logic programming language.
These queries can be answered on-line which enables the analysis of
traces of large size. The tool can be used for program debugging and we
are now
investigating its use in intrusion detection.
We have proposed a method for the automatic
generation of test cases. This method forms the kernel of the CASTING
tool, developed in collaboration with the SME ``AQL''. CASTING can take
input programs and specifications written in a variety of languages and
will produce test cases according to a test strategy chosen by the
user. We are currently adapting CASTING to test case generation
from UML specifications.
