1. Archives

1. Archives

Équipe Modélisation et développement logiciel avancé

 

Jeu d’outils incluant plusieurs modules de modélisation et d'analyse capables de traiter des traces provenant de différents types de systèmes

Nous avons développé un jeu d'outils incluant 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écifications à base de patrons de propriétés (80 patrons largement utilisés dans le domaine), ainsi que l'interface utilisateur graphique. 
Partenaire : Siemens AG

 

Outil prototype pour la validation formelle de systèmes de contrôle d’accès à base de rôles

Nous avons développé un outil prototype pour la validation formelle de systèmes de contrôle d’accès à base de rôles (Role Based Access Control ou RBAC) étant donné un ensemble de workflows sur lesquels ces systèmes de contrôle opèrent. Le système à vérifier est composé du RBAC et d’un ou de plusieurs workflows, contrôlés par ce RBAC et définis pour un ensemble d’usagers.

 

Outils prototype pour la détection des bogues dans les applications Java multithread

Un outil prototype pour la détection des bogues dans les applications Java multithread a été développé. Des douzaines d’antipatrons ont été documentés et des modules de détection pour dix d’entre eux ont été implémentés dans le prototype. L’outil a été étendu avec une approche d’analyse dynamique basée sur le développement d’observateurs (implantés sous forme d’automates), l’enregistrement de l’activité de l’application dans des fichiers journaux et l’analyse de ceux-ci par model checking. Un outil d’aide à la migration de code Java (de la version 1.4 à la version 1.5 de la Java Virtual Machine ou JVM), un prototype d’un outil avancé de génération de code basé sur la notion de métacomposant et un prototype de génération de code ont été développés.

 

Outils prototypes pour l’automatisation des activités de vérification de tests en collaboration avec Siemens AG

Les chercheurs du CRIM élaborent des méthodes à base de modèles et développent des outils prototypes pour l'automatisation des activités de vérification de tests. 
Partenaire : Siemens AG

 

 

Preuve de concept d’un module de corrélation d’événements pour le contrôle embarqué

Une preuve de concept d’un module de corrélation d’événements pour le contrôle embarqué a été développée, permettant d’analyser les traces SNMP (Simple Network Management Protocol) produites par les appareils embarqués et de faire la corrélation avec les activités réseaux anormales (comme des paquets erronés et des paquets perdus) en certains points du réseau.

 

Preuve de concept d’un outil d’adaptation de tests

Résumé : Les applications sont fréquemment soumises à des changements au cours de leur cycle de vie et les activités de test sont particulièrement touchées par ces changements.

Résultat : Dans ce contexte, nous avons développé une preuve de concept d’un outil d’adaptation de tests. Un modèle formel de l’application ainsi qu’un ensemble valide de tests sont fournis à l’outil. Étant donné un modèle formel de la version suivante de l’application, l’outil identifie les tests toujours valides sur cette nouvelle version ainsi que ceux qui doivent être mis à jour. Pour les tests invalides, l’outil détecte les premières étapes qui ne sont plus compatibles avec la nouvelle version. Ces informations permettent au développeur de vérifier rapidement de grands jeux de tests et de ne mettre à jour que le nombre minimum de ceux-ci. Des extensions possibles de ce travail incluent la mise à jour automatisée des tests et la génération de tests supplémentaires pour la nouvelle version de l’application.

 

WebFIM – Automatisation de la vérification de propriétés dans les applications Web

Résumé : Le but de ce projet de recherche interne est d'automatiser la vérification de propriétés dans les applications Web. 

Résultat : 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 SPIN (model-checker) à 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.

 

Équipes

Nouvelles récentes

  • Projet en vitrine : Le Solutionneur
    15/09/2017

    Saviez-vous que Le Solutionneur a été utilisé par 120 écoles secondaires du Québec pour confectionner les horaires pour la rentrée scolaire 2017 de 101 000 élèves ?

    +

Événement à venir

  • Technologies émergentes, tendances et perspectives
    2/10/17 8h30
    Université Laval - Pavillon Desjardins (Québec)
    Une conférence d'ISACA-Québec en partenariat avec le CRIM qui se tiendra le 2 octobre 2017 à l'Université Laval à Québec.
    +
  • Saviez-vous que Le Solutionneur a été utilisé pr 120 écoles sec QC pr faire horaires #rentree2017 de 101 000 élèves… https://t.co/b2Nr7NfJrD
  • CRIM is happy to present 2 papers at #IWCS2017! https://t.co/wcH8i2mTdZ https://t.co/Hc9IDNvwhj

Publications récentes

  • PeopleBot

    +
  • Fine-grained domain classification of text using TERMIUM Plus

    +