Outils d'analyse statique et de vérification pour les ...

De
Publié par

  • rapport de stage - matière potentielle : outils d' analyse statique et de vérification pour les applications java distribuées
  • rapport de stage
Christophe Massol IUP MIAGE Nice Année 2002/2003 INRIA – Projet OASIS 2004 route des Lucioles BP 93 06902 Sophia Antipolis Enseignant Responsable: Olivier Dalle Responsable du stage dans l'entreprise : Eric Madelaine Outils d'analyse statique et de vérification pour les applications Java distribuées Rapport de stage
  • modèle intermédiaire
  • optimisation de systèmes complexes
  • optimisation des systèmes complexes
  • structure du programme distribué
  • maintenance d'applications
  • modification du module jjjc
  • module abstraction
  • module d'analyse statique de classes
  • java
  • équipes de recherche
  • équipe de recherche
  • équipes de la recherche
  • equipe de recherche
  • équipes de recherches
  • analyse
  • analyses
Publié le : mercredi 28 mars 2012
Lecture(s) : 98
Source : www-sop.inria.fr
Nombre de pages : 40
Voir plus Voir moins

Christophe Massol IUP MIAGE Nice
Chris.massol@free.fr Année 2002/2003
Outils d’analyse statique
et de vérification pour les
applications Java distribuées
Rapport de stage
INRIA – Projet OASIS Enseignant Responsable:
2004 route des Lucioles Olivier Dalle
BP 93 Responsable du stage dans l’entreprise :
06902 Sophia Antipolis Eric MadelaineRapport de stage Outils d’analyse statique et
de vérification pour les
applications Java distribuées
REMERCIEMENTS
Je remercie tout particulièrement l’INRIA qui m’a permis d’effectuer un stage
intéressant et enrichissant.
Je remercie également Monsieur Eric Madelaine ainsi que Madame Rabéa Boulifa
pour toute leur aide apportée sur la compréhension du sujet ainsi que leurs précieuses
explications.
Je remercie Monsieur Olivier Dalle pour son accompagnement tout au long du stage.
Enfin, je tiens à remercier le personnel de l’INRIA pour son accueil et sa sympathie.
Christophe Massol Année 2002-2003 Page 2 sur 40Rapport de stage Outils d’analyse statique et
de vérification pour les
applications Java distribuées
SOMMAIRE
INTRODUCTION ........................................................................................................................................................ 5
1 PRESENTATION DE L’ENTREPRISE........................................................................................................ 6
2 LE PROJET OASIS ........................................... 8
2.1 LA LIBRAIRIE PROACTIVE................................................................................................ 8
2.2 ENVIRONNEMENT D’ANALYSE ET DE VERIFICATION....................... 9
3 OBJECTIFS DU STAGE ................................12
3.1 PRESENTATION DU STAGE..............................................................................................12
3.2 PLAN DE TRAVAIL PREVISIONNEL..................................................13
4 LES LOGICIELS BANDERA ET SPARK.................................14
4.1 DESCRIPTION DE BANDERA............................................................................................................................14
4.1.1 Module de transformation Java -> Jimple (JJJC) ............................................................................14
4.1.2 Module d’analyse statique de classes15
4.1.3 Module d’extraction de propriétés (Property Extractor).15
4.1.4 Module de découpage (Slicing)..........................................15
4.1.5 Module abstraction .............................................................................................16
4.1.6 Module BIR (Bandera Intermediate Representation).......................................16
4.1.7 Module de vérification (Model Checking).........................................................16
4.2 FONCTIONNEMENT DE BANDERA...................................................16
4.3 LIMITES DU LOGICIEL B....................................................17
4.4 MODULE ABSTRACTION PROPOSE PAR BANDERA.........................17
4.4.1 Définition de l’abstraction..................................................17
4.4.2 Module Abstraction dans Bandera.....................................................................18
4.4.2.1 Le langage BASL ............................................................................................... 18
4.4.2.2 L’interface utilisateur.......................... 19
4.4.2.3 Résultats de l’abstraction..................................................... 19
4.4.3 Utilisation du module d’abstraction pour un programme utilisant la librairie ProActive ............19
4.5 SPARK : OUTIL D’ANALYSE STATIQUE DE POINTEURS SUR LANGAGE JIMPLE..............................................19
4.5.1 Utilisation de Spark dans notre analyse ............................................................21
5 TRAVAUX EFFECTUES...............................................................................................23
5.1 ADAPTATION DE BANDERA A PROACTIVE....................................................................24
5.1.1 Modification du module JJJC.............................................25
5.1.2 Prise en compte de ProActive25
5.2 INTEGRATION DES OUTILS D’ANALYSE DE CLASSE LANDE...........26
5.3 ANALYSE STATIQUE DES OBJETS ACTIFS .......................................................................27
5.3.1 L’analyse des objets actifs..................................................28
5.3.2 La structure Jimple..............................................................................................28
5.3.2.1 Jimple – Nœud Affectation.................. 29
5.4 ANALYSE STATIQUE DES LIENS DE COMMUNICATION...................31
5.4.1 Adaptation de Spark pour une analyse d’un code basé sur la librairie ProActive.........................31
5.4.1.1 Intégration de l’appel constructeur....................................................................................................... 32
5.4.1.2 Intégration de l’appel à la méthode runActivity..................... 33
5.4.2 Identification d’une communication vers un objet actif...33
5.4.3 Limites de l’analyse.............................................................................................................................34
5.4.4 Identification d’une instance d’un objet actif à un point donné.......................34
5.5 PLANNING RECAPITULATIF35
5.6 AVANCEMENT.................................................................................................................................................37
5.6.1 Les fonctionnalités implémentées.......37
5.6.2 Les fonctionnalités non terminées......37
Christophe Massol Année 2002-2003 Page 3 sur 40Rapport de stage Outils d’analyse statique et
de vérification pour les
applications Java distribuées
5.6.3 Les problèmes ouverts.........................................................................................................................37
CONCLUSION ...........................................................38
REFERENCES................................................................................................39
Christophe Massol Année 2002-2003 Page 4 sur 40Rapport de stage Outils d’analyse statique et
de vérification pour les
applications Java distribuées
INTRODUCTION
Afin de développer mes connaissances avec profit et m’initier à la vie d’entreprise,
l’enseignement universitaire professionnel de la MIAGE propose un stage de fin d’étude de
25 semaines (du 3 Mars au 31 août).
Parmi les nombreuses propositions, mon choix s’est porté sur l’INRIA.
Cet institut, spécialisé dans la recherche informatique, est toujours à la pointe de la
technologie intégrant nombre de chercheurs de diverses nationalités.
J’ai évolué dans le projet OASIS, projet dont le but est d’offrir des outils pour la
construction, l’analyse, la vérification et la maintenance d’applications réparties Java. J’ai été
intégré dans l’équipe Vercors.
Christophe Massol Année 2002-2003 Page 5 sur 40Rapport de stage Outils d’analyse statique et
de vérification pour les
applications Java distribuées
1 Présentation de l’entreprise
L’INRIA est un institut publique de recherche en informatique et automatique créé en
1967 par les ministères de la recherche, de l’économie, des finances et de l’industrie.
Les buts de cet institut sont de réunir les compétences du dispositif de recherche français afin
de développer les nouvelles technologies qui sont un des moteurs important de notre
économie, partager ses connaissances dans un cadre international, assurer la diffusion de son
savoir, contribuer à la normalisation ainsi que de réaliser des expertises dans le domaine
informatique. Cet institut doit également réaliser des programmes de coopération avec
d’autres structures pour le développement des nouvelles technologies et réaliser des systèmes
expérimentaux.
Cette vocation envers la haute technologie se traduit par des publications de concepts et
de connaissances dans la littérature scientifique mais également par des logiciels et prototypes
expérimentaux novateurs (comme exemple, nous pouvons citer la librairie ProActive –
développée par le projet OASIS sur le site de Sophia Antipolis – qui facilite la programmation
répartie Java entre plusieurs machines virtuelles). Pour mener à bien tous ses projets, l’INRIA
met en place des partenariats avec le CNRS, les écoles d’ingénieurs, les universités, les
industries ainsi que des relations européennes et internationales.
Cet établissement est partagé en 6 sites indépendants qui lui permettent de renforcer sa
présence sur le territoire et de multiplier les partenariats. J’ai été intégré dans l’unité de
recherche de Sophia Antipolis dirigée par Michel Cosnard. Cette unité a été créée en 1982
dans la plus grande technopole européenne. Elle intègre aujourd’hui 455 personnes formant
28 équipes de recherche. Ces équipes couvrent des sujets très variés de l’informatique et de
l’automatique avec quatre thèmes principaux :
• Réseaux et systèmes ;
• Génie logiciel et calcul symbolique ;
• Interaction homme-machine, images, données et connaissances ;
• Simulation et optimisation des systèmes complexes.
Christophe Massol Année 2002-2003 Page 6 sur 40Rapport de stage Outils d’analyse statique et
de vérification pour les
applications Java distribuées
Une équipe de recherche est organisée autour de 10 à 25 scientifiques. Elle intègre des
chercheurs permanents de l’INRIA mais elle peut également intégrer des ingénieurs, des
étudiants en thèse ainsi que des stagiaires ponctuels venant de diverses écoles. Elle est dirigée
par un directeur de projet (personne habilitée à diriger des projets) et sa durée de vie est d’au
plus douze ans.
Christophe Massol Année 2002-2003 Page 7 sur 40Rapport de stage Outils d’analyse statique et
de vérification pour les
applications Java distribuées
2 Le projet OASIS
Le projet OASIS (Ref 15), créé par l’initiative d’Isabelle Attali en juin 1999, est un projet
commun entre l’INRIA, le CNRS et l’UNSA. Son but est de proposer dans un contexte
d’applications réparties des principes, techniques et outils pour la construction, l’analyse, la
vérification et la maintenance de systèmes.
Le projet a été créé dans le contexte de l’explosion de l’Internet, du partage de
l’information et de l’avènement du langage Java. La problématique du projet est exprimée par
la difficulté liée à la programmation et à la maintenance d’applications réparties Java. Les
objectifs sont alors de définir une plate-forme d’aide à la programmation ainsi qu’une plate-
forme de développement, d’analyse et de vérification d’applications réparties sur un réseau
local (LAN), sur un système de clusters ou sur le réseau Internet.
2.1 La librairie ProActive
La librairie Java ProActive (Ref 14) est la solution de l’équipe OASIS face à l’absence
de bibliothèque basée sur la programmation de systèmes répartis. Elle est basée sur la JVM
(Java Virtual Machine) Java de SUN et utilise le protocole meta-objet structuré sur la librairie
RMI pour assurer le transport de l’information.
Concrètement, ProActive propose des primitives permettant de simplifier la
programmation d’applications distribuées en Java et d’en garantir la sécurité (Figure 1). Cette
librairie introduit la notion d’objets actifs.
Objet distribué
LibrairieA Objet distribué
ProActive C
Objet distribué JVM BGarantie de sécuritéBJVM A
Figure 1: Communication ProActive
Christophe Massol Année 2002-2003 Page 8 sur 40Rapport de stage Outils d’analyse statique et
de vérification pour les
applications Java distribuées
Un objet actif est un objet distribué par la librairie ProActive sur un réseau. Il peut alors
effectuer des appels distants vers d’autres objets actifs sur le réseau ainsi que réceptionner des
appels distants provenant d’autres objets actifs et y répondre. (Figure 2).
Object actif
Objet passif
Figure 2 : Communication distribuée
Proxy
Object
Body
Figure 3 : Objet Actif
Un objet actif dispose d’une queue de requêtes (appels passés par l’intermédiaire de la
librairie ProActive) représentée sur la Figure 3 par l’objet Body.
La librairie ProActive permet à l’utilisateur de définir le comportement des objets
actifs. Le comportement de ces objets est caractérisé par la politique de traitement vis-à-vis
des appels distants. Il est défini par l’utilisateur par la surcharge sur tout objet actif de la
méthode runActivity liée à la librairie ProActive.
2.2 Environnement d’analyse et de vérification
L’équipe OASIS développe également un environnement d’analyse et de vérification de
programmes dans le cadre de systèmes Java distribués : la plate-forme VERCORS
(VERification de modèles pour COmposants Répartis communicants, surs et Sécurisés). Cette
analyse repose sur la définition de modèles comportementaux définissant le comportement
temporel des objets de l’application. En utilisant des outils de vérification basés sur ces
Christophe Massol Année 2002-2003 Page 9 sur 40Rapport de stage Outils d’analyse statique et
de vérification pour les
applications Java distribuées
modèles comportementaux, des analyses peuvent être conduites afin de s’assurer du bon
comportement (recherche d’inter-blocages, propriétés de sûreté).
Ces développements reposent sur les travaux des membres de l’équipe (Ref 1): définition
d’une sémantique pour ProActive, d’un modèle intermédiaire (système d’automates
paramètrés) pour exprimer les comportements, analyse statique permettant de déterminer
certaines propriétés des applications.
Code
utilisateur
Analyse de la
structure de
l’application
Objets Liens de
distribués communication
Calcul des
comportements
Modèle
compositionnel
paramètré
Vérification
par moteur
d’analyse
Figure 4 : Plate-forme Vercors
L’architecture de Vercors (Figure 4) repose sur la source Java du code utilisateur
interprétée dans un langage intermédiaire proche du Bytecode, facile à analyser. La plate-
forme va analyser la structure du programme distribué. Il est alors important de collecter les
informations liées à la librairie ProActive :
• Les objets actifs créés par l’application ;
• Les points de communication entre objets actifs.
Christophe Massol Année 2002-2003 Page 10 sur 40

Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.