LANDE Research team
Software design and validation
- Leader : Thomas Jensen
- Research center(s) : CRI Rennes - Bretagne Atlantique
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Programs, Verification and Proofs
- Partner(s) : Université Rennes 1,Ecole normale supérieure de Cachan,CNRS,Institut national des sciences appliquées de Rennes
- Collaborator(s) : U. RENNES 1, CNRS, INRIA, INSA RENNES, CENTRALESUPELEC, ENS RENNES, INSTITUT MINES-TELECOM, UBS
The LANDE project-team 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.
Research themesThe 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.
Keywords: Program development Debugging Test Validation Verification Static analysis Dynamic analysis Type Software architecture Functional language Logic programming Programming environment Software engineerin