|
Les activités de recherche et de développement de l'équipe Analyse de
systèmes distribués (ASYD) du CRIM couvrent les cinq thèmes suivants :
Analyse des systèmes distribués basée sur des patrons
L'équipe a développé un ensemble d'approches basées sur la technologie des patrons (largement
adoptée dans le monde du développement logiciel), afin de réduire le coût et la complexité de ces
activités dans les systèmes distribués. De plus, elle a élaboré des bibliothèques de patrons de
propriétés et d'erreurs prédéfinies applicables à plusieurs domaines :
Analyse automatisée des traces des systèmes distribués
L'équipe développe une approche et un ensemble d'outils pour l'analyse des systèmes distribués à
partir de leurs traces d'exécution (logfiles). Une trace collectée est utilisée pour produire un modèle formel, qui est
ensuite vérifié à l'aide de propriétés définies par les utilisateurs. Ces propriétés spécifient les
exigences fonctionnelles et non fonctionnelles de l'application analysée.
La collaboration sur ce sujet avec la firme
Siemens AG (qui se poursuit
depuis 2001) a résulté principalement en un jeu d'outils. Ceux-ci incluent plusieurs modules de
modélisation et d'analyse capables de traiter des traces provenant de différents types de systèmes
(tels que les réseaux de télécommunications GSM et UMTS et les systèmes de contrôle de trafic des
trains), une bibliothèque de spécification à base de patrons de propriétés (80 patrons largement
utilisés dans le domaine), ainsi que l'interface utilisateur graphique.
Vérification des applications Web
Le but de ce projet de recherche interne est d'automatiser la vérification de propriétés dans
les applications Web. Un prototype de vérification a été implémenté, dans lequel le butinage d'une
application Web permet de représenter celle-ci en un modèle, exprimé sous forme d'automates, et
vérifiée par le vérificateur formel (model-checker) Spin à l'aide de propriétés définies par
l'utilisateur. Le prototype est équipé d'une interface graphique avancée qui facilite la
spécification des propriétés.
Analyse statique des applications
multithread Java
Ce projet, réalisé en collaboration avec
SAP, vise à découvrir les sources de
bogues dans des applications
multithread Java à partir du seul code source de ces applications. L'équipe a documenté
38 patrons de bogues (aussi
appelés antipatrons) typiques pouvant être présents dans le code source d'une application. Elle a
aussi proposé une classification de ces antipatrons et des modules de détection pour identifier
plusieurs d'entre eux.
Analyse dynamique des applications
multithread Java
Il est difficile de détecter la totalité des bogues découlant de l'utilisation de plusieurs
threads au sein d'une même application à l'aide de la seule analyse statique. Dans ce
projet interne, l'équipe a conçu une technique d'analyse dynamique, basée sur le développement
d'observateurs représentés sous forme d'automates et sur l'utilisation de méthodes de vérification
formelle (model-checking).
Méthodologies de test à base de modèles
Les méthodologies à base de modèles permettent l'automatisation, l'amélioration et la réduction
du coût des activités de test. Les modèles utilisés sont en général des représentations partielles
et abstraites des fonctionnalités, comportements, architectures et données du système testé.
L'équipe utilise également des modèles de tests et de fautes afin d'améliorer la qualité de
l'activité de test. Cette recherche inclut les axes suivants :
Adaptation automatique de tests pour des applications d’affaires changeantes
Les logiciels sont continuellement modifiés au cours de leur cycle de vie. C’est
particulièrement le cas des applications de gestion d'affaires, en constante évolution, afin de
répondre aux exigences variables et aux changements structurels des entités commerciales auxquelles
elles se destinent. Les phases du cycle de développement logiciel les plus touchées par de telles
modifications sont le test et la validation. Il s'agit là de deux tâches complexes,
particulièrement dans le cas des applications larges et complexes.
En collaboration avec
SAP, l'équipe s’est penchée sur le
problème de l'amélioration des processus de test, en prenant en considération les changements subis
par une application. Elle développe une approche à base de modèles et un outil prototype pour la
détection des changements et l'adaptation automatisée des tests aux applications changeantes.
Vérification à base de modèles des tests des systèmes distribués
La qualité des tests est cruciale pour les systèmes complexes que sont les systèmes distribués.
Pourtant, les tests dédiés à ces systèmes sont dans la plupart des cas développés manuellement. Ils
peuvent donc contenir fautes et incohérences, spécialement en l'absence de toute spécification
formelle du système testé. En collaboration avec
Siemens AG, les chercheurs
élaborent des méthodes à base de modèles et développent des outils prototypes pour l'automatisation
des activités de vérification des tests.
Génération de tests pour les systèmes distribués
En collaboration avec
France
Télécom R&D, l'équipe a étudié la génération automatique de tests à partir des
spécifications des systèmes distribués en utilisant des techniques de vérification formelle
(model-checking).
L'approche proposée de génération de tests est basée sur la modélisation d'un système distribué
par un système de machines à états finis étendues communicantes (CEFSM). Ce modèle général combine
à la fois le flux de commande et les données. Il permet de traiter la couverture du
modèle d'un système en termes de spécification et de fautes.
Test à base de modèles
L'objectif principal de ce projet de recherche financé par le
CRSNG est de contribuer au
développement de nouvelles méthodes et technologies à base de modèles pour tester les systèmes
distribués. Ce faisant, il faut également tenir compte des caractéristiques fondamentales comme le
parallélisme, le non-déterminisme et les communications asynchrones.
Sécurité des logiciels
L'équipe a conçu des systèmes destinés à assurer la sécurité des réseaux informatiques ainsi que
de leurs utilisateurs. Ses travaux concernent trois aspects :
- La vérification formelle de la sécurité des logiciels
- La conception de systèmes de détection et de prévention d'intrusion
- La protection personnelle des utilisateurs
Vérification de contrôle d'accès à base de rôles dans les processus d'affaires
En collaboration avec
SAP, l'équipe a développé une approche
formelle pour la validation des systèmes de gestion de droits d'accès à base de rôles. Une machine
à états finis étendue (EFSM) est utilisée pour représenter les processus d'affaires (définis comme
des flux de travail) ainsi que les règles de contrôle d'accès associées. Le vérificateur formel
(model-checker) Spin est utilisé pour tester une variété de propriétés (concernant, par exemple, la
séparation des devoirs).
Système multi-agent distribué sécuritaire
Dans le cadre de collaborations avec les entreprises
SecureOps et ReactSys,
l'équipe a développé des approches pour la conception d'architectures distribuées permettant la
détection des attaques ainsi que leur prévention en temps réel. Ces architectures sont basées sur
un modèle d'agents coopératifs non mobiles capables d'inférer les intentions des intrus
potentiels.
Filtrage basé sur le contenu des accès WWW
En collaboration avec
FokusMedia, l'équipe a
étudié des modèles de filtrage des accès au World Wide Web, afin d'empêcher les utilisateurs
d'accéder à certains sites Web. Elle a aussi proposé une nouvelle architecture transparente
reposant sur l'utilisation du service DNS combinée avec un filtrage des pages par leur contenu.
Développement de systèmes informatiques distribués intelligents
L'équipe étudie et conçoit des systèmes de calcul distribué intelligents, des systèmes pour la
planification automatique de contingences et des systèmes de gestion des emplois du temps. Les
avenues de recherche explorées sont reliées aux systèmes multi-agents, aux réseaux pair-à-pair et à
l'intelligence artificielle.
Plateforme pour applications en ligne distribuées
En collaboration avec
TEC, l’équipe conçoit une plateforme
logicielle de distribution de logiciels. Deux aspects sont pris en considération :
- L'hôte du logiciel distribué est protégé contre les malveillances possibles du logiciel.
- Le logiciel s'exécute dans un environnement protégé garantissant l'intégrité de son code et sa
non-redistribution si celle-ci n'est pas expressément autorisée.
L'utilisation des logiciels distribués à travers la plateforme est mesurée, à des fins par
exemple de facturation à l'usage.
Planification automatique
Dans ce projet en collaboration avec
Recherche et développement pour la défense
Canada (RDDC), l'équipe étudie les systèmes de planification de contingences. La performance et
les limites des systèmes existants sont étudiées et une approche alternative basée sur des méthodes
formelles est proposée.
Emplois du temps
Soutenu par la
Commission
scolaire de Laval et effectué en collaboration avec l’équipe Développement et technologies
Internet du CRIM, ce projet concerne la production automatique d'emplois du temps pour les écoles
secondaires du Québec. La génération d'emplois du temps prend en compte les particularités des
écoles (nombre d'étudiants, taille de l'école, etc.), cours, préférences des professeurs, choix des
étudiants, ainsi qu'un ensemble complémentaire d'exigences globales.
Analyse statique de logiciels
L'analyse statique de logiciels repose principalement sur la disponibilité du code source. Elle
permet ainsi d'analyser un logiciel à l'extérieur de son environnement d'exécution.
Inspection et diagnostic de programmes par analyse du code source
Valider la qualité de la conception et de l'implémentation d'un logiciel nécessite des moyens
spécialisés capables de faciliter l'analyse du code source du logiciel. Une telle analyse permet la
détection des défauts tels que la violation des normes de conception et des conventions de
codage.
D'autres types de détection plus spécifiques peuvent être réalisés sous forme de mise en
application d'heuristiques de qualité largement adoptées par la communauté de développement
logiciel.
Enfin, différentes métriques peuvent également être construites, afin de fournir une évaluation
quantitative de la qualité du code source.
Détection des problèmes reliés à la migration dans les applications Java
Dans ce projet réalisé avec
SAP, l'équipe a étudié les effets de la
migration de la version 1.4 à la version 1.5 de Java. Elle a établi la liste des problèmes posés
par cette migration. Les problèmes identifiés ont été regroupés en catégories et des détecteurs
capables de signaler la présence de ces problèmes dans le code ont été développés.
Les chercheurs ont offert une liste de recommandations et de conseils permettant aux
développeurs d'éviter ces problèmes à l'avenir.
|
