Conception et validation de logiciel
Présentation du projet
Projet commun avec l'INSA de Rennes,
l'Université de Rennes 1 et le CNRS.
Le thème de recherche central du
projet Lande est la conception d'outils d'aide au développement
et à la validation de logiciels. Notre approche est
fondée sur une collection de méthodes
formelles permettant de spécifier ou d'extraire une vue
partielle de l'architecture et du
comportement d'un logiciel. Cette approche nous a amenés
à étudier deux types de problèmes.
D'une part, la spécification d'un logiciel en vues partielles
nécessite une vérification de la
cohérence entre plusieurs vues afin que celles-ci puissent
être synthétisées. D'autre part,
l'extraction d'une vue demande des techniques d'analyse statique et
dynamique précises. Nous
insistons sur la nécessité que les réponses
apportées à ces problèmes reposent sur des bases
formelles (sémantique du langage étudié,
définitions de propriétés à vérifier
dans des logiques
formelles) afin d'obtenir une garantie sur les résultats
produits. De plus, il est important que les
outils construits soient le plus automatiques possible car les
utilisateurs visés ne sont pas
nécessairement des experts en méthodes formelles.
Axes de recherche
La description multi-vues de
l'architecture de gros logiciels a comme objectif de spécifier
l'organisation globale de systèmes afin d'améliorer la
maîtrise de leur développement
(spécification, analyse, programmation, test, maintenance,
etc.). Une ambition majeure dans ce
domaine est le passage à l'échelle de techniques comme
l'analyse, le raffinement ou la vérification
de programmes. Nos travaux visent à assurer une forme de
cohérence de ces descriptions
hétérogènes. Le défi principal est de
trouver comment mettre en relation des vues qui mettent en
jeu des propriétés de nature très
différentes ou qui se situent à des niveaux d'abstraction
différents. Une fois les vues mises en relation, il devient
possible d'utiliser des techniques
standards d'analyse statique ou de vérification afin d'assurer
des propriétés de cohérence.
La nouvelle technique de programmation
appelée « programmation par aspects »
consiste à
décrire un logiciel comme un ensemble formé d'un
composant principal et d'une collection de
vues ou d'aspects décrivant des tâches comme la gestion
mémoire, la synchronisation, les
optimisations, etc. Un outil, appelé tisseur, est chargé
de produire automatiquement un programme
intégrant les différents aspects au composant principal.
L'intérêt de cette approche est de localiser
(dans les aspects) des choix de mise en oeuvre qui seraient sinon
dispersés dans le code source.
Après avoir proposé un aspect dédié
à la sécurisation de code mobile, nous avons
étudié les
problèmes d'interactions qui se posent lorsque l'on doit tisser
plusieurs aspects. En effet, comme
pour les vues, les aspects ne sont pas obligatoirement orthogonaux et
des conflits ou ambiguïtés
peuvent apparaître lors du tissage. Nous travaillons
également sur un langage d'aspect dédié à la
composition de composants.
Pour faciliter la navigation et
l'organisation de logiciels de taille importante nous cherchons à
définir un cadre logique pour les systèmes
d'information qui décrit uniformément la navigation,
l'interrogation et l'analyse des données. Ce cadre est
générique par rapport à la logique utilisée
pour naviguer et interroger ; en particulier il peut être
appliqué à plusieurs types de logiques de
programme, comme les types ou des propriétés statiques.
Ces travaux se basent sur une extension
de la théorie de l'analyse de comcepts.
La validation d'un logiciel utilisent
des méthodes d'analyses et de test de programmes. Nous
nous intéressons à différents aspects de l'analyse
statique de programmes, aussi bien sur le plan
des fondements (spécification d'analyses à partir de
règles d'inférence) que des applications
(détection des pointeurs pendants pour l'aide à la mise
au point de programmes C, analyse de flot
de données et de contrôle dans des programmes Java et Java
Card, analyse de protocoles
cryptographiques) et à la mise en oeuvre d'analyses statiques
par des techniques de résolution
itérative de systèmes d'équations et de
réécriture d'automates d'arbres.
Pour faciliter l'analyse dynamique
de programmes, nous développons un outil d'analyse de traces
d'exécution permettant à l'utilisateur d'exprimer des
requêtes dans un langage de programmation
logique. Ces requêtes peuvent être traitées à
la volée, ce qui permet d'analyser des traces de
grande taille. L'outil peut être utilisé pour le
débogage de programmes séquentiels et nous
étudions maintenant son application au problème de la
détection d'intrusion.
En collaboration avec la
société AQL nous poursuivons le développement de
l'outil casting dont
le noyau utilise une méthode de génération de
suites de tests. L'outil peut prendre des entrées
dans des formats variés et produit des suites de tests selon des
stratégies spécifiées par
l'utilisateur. Nous adaptons actuellement casting pour la
génération de suites de test à partir de
spécifications UML.
La sécurité logicielle
constitue un domaine d'application
privilégié pour le projet. Nous
élaborons un cadre pour la définition de
propriétés de sécurité et une technique
pour leur
vérification automatique. Cette technique intègre des
techniques d'analyses statiques et de
vérification de modèle (« model checking »).
Ce cadre a été appliqué à la formalisation
et la
vérification de politiques de sécurité
d'applications programmées avec la nouvelle architecutre de
sécurité de Java 2 et à la vérification de
propriétés de sécurité des cartes à
puce
multi-applicatives programmées avec le langage Java Card.
Responsable scientifique
Thomas Jensen
+33 2 99 84 74 78
Thomas.Jensen@irisa.fr
Secrétariat : +33 2 99 84 25 77
Les projets
du même thème
|
