Forge
Logiciels MoVe
BCM4Java : Modèle à composants basique pour Java
Ce projet est une implantation d'un modèle de programmation par composants répartis en Java (20.000 lignes de code et de documentation environ à ce jour, sous GitHub). Il propose les principaux concepts de l'approche à base de composants : composants logiciels, interfaces de composants, ports exposant les interfaces requises et offertes par les composants, et connecteurs explicites. Utilisant la technologie Java RMI, il permet une programmation répartie grâce au déploiement de composants sur différentes machines virtuelles Java (s'exécutant sur différents ordinateurs) et aux appels inter-composants via RMI. Débuté dans le cadre du projet de recherche ANR SALTY où il a permis de développer une application déployant 10.000 composants répartis, ce logiciel a été utilisé par quelques centaines d'étudiants et il l'est toujours d'abord dans le cadre du cours de master 2 ALASCA depuis 2014, puis dans le cadre du cours de master 1 Composants depuis 2019.
Project Leader : Jacques MALENFANT
11/2012
BCMCyPhy : Modèle à composants pour les systèmes de contrôle cyber-physiques
Ce projet de recherche et le logiciel associé visent à concevoir et implanter un modèle de programmation par composants pour les systèmes de contrôle cyber-physique. Il se greffe sur le projet BCM4Java dont il utilise les concepts de base et l'implantation des composants répartis en Java (10.000 lignes de code et de documentation à ce jour). Outre le fait d'intégrer des composants temps réel, ce projet étudie les architectures de contrôle (automatique) à base de composants, leur spécification utilisant les systèmes hybrides stochastiques et leur simulation utilisation des modèles de simulation suivant la norme DEVS. Une attention particulière est portée sur la composabilité parallèle entre les composants, leurs spécifications et leurs modèles de simulation individuels. Un sous-projet logiciel de BCMCyPhy propose une nouvelle implantation en Java de la norme DEVS pour la simulation modulaire des composants et de leurs assemblages (20.000 lignes de code et de documentation à ce jour)). Les simulateurs obtenus par composition entre simulateurs de chaque composant permettent ensuite de mettre au point, tester, vérifier et valider les applications. Ce logiciel a été utilisé par quelques dizaines d'étudiants et l'est toujours dans le cadre du cours de master 2 ALASCA depuis 2018.
Project Leader : Jacques MALENFANT
06/2019
BUT4Reuse : Bottom-Up Technologies for Reuse
BUT4Reuse provides a unified framework for mining software artefact variants: Commonality and variability analysis, Feature identification, Feature location, Feature constraints discovery, Feature model synthesis, Reusable assets construction. It is easily extensible and currently supports several artefact types: Java, C, EMF Models, Textual files, File structures, JSON and CSV files, and much more.
Project Leader : Tewfik ZIADI
01/2017
Cosy : Contrôleur de symétries
Cosy est une bibliothèque C++ efficace conçue pour casser dynamiquement les symétries dans la résolution de problèmes SAT. Elle s'appuie sur des solveurs SAT de l'état de l'art en intégrant un contrôleur de symétrie qui fonctionne de manière complémentaire avec l'algorithme CDCL (Conflict-Driven Clause Learning). Cosy peut être intégré à la plupart des solveurs CDCL, offrant flexibilité et performance améliorée, notamment dans les instances SAT hautement symétriques. Elle est disponible sous licence open-source GPL v3.
Project Leader : Souheib Baarir
04/2018
CosyVerif : Environnement logiciel pour la spécification et la vérification de systèmes dynamiques
CosyVerif est un environnement logiciel permettant la spécification formelle et la vérification de systèmes dynamiques.
Project Leader : Fabrice KORDON
06/2019
CPN-AMI est un environnement conçu sur FrameKit: une plate-forme logicielle d'intégration permettant un couplage rapide d'outils de provenance diverses. CPN-AMi est ainsi l'assemblage le plus complet d'outils de vérifications à partir de réseaux de Petri. Ces outils ont été développés dans le cadre des travaux de SRC ou par des partenaires universitaires (Université de Turin, Université d'Helsinki, Bell-Labs, Université de Munich, Université Humbolt à Berlin). CPN-AMI est composé d'un serveur d'outils et d'une interface utilisateur déporté à laquelle on se connecte.
Project Leader : Fabrice KORDON
12/1994
DDD : Bibliothèque de manipulation des Data Decision Diagrams
La libDDD est une bibliothèque de manipulation des Data Decision Diagrams et des Hierarchical Set Decision Diagrams. Elle supporte flexiblement des types de données complexes et las algorithmes de "saturation", offrant à ses utilisateurs des performances au sommet de l'état de l'art. Cette bibliothèque C++ est distribué sous les termes de la LGPL de Gnu.
Project Leader : Yann THIERRY-MIEG
01/2001
ITS-Tools : Vérification symbolique multi-formalisme
ITS Tools est un model-checker symbolique acceptant en entrée un large éventail de formalismes et vérifiant des propriétés de sûreté, mais aussi des formules LTL et CTL.
Project Leader : Yann THIERRY-MIEG
01/2015
LfP : Language for Prototyping
Il s'agit d'un langage de spécification de systèmes répartis à partir duquel nous travaillons pour générer automatiquement des spécifications formelles et des programmes. Le compilateur de ce langage a été écrit et intégré dans la plate-forme FrameKit (à coté de l'environnement CPN-AMI pour permettre un couplage et exploiter les outils de vérification). Ce langage et son compilateur sont à l'origine de notre participation dans le projet RNTL MORSE
Project Leader : Fabrice KORDON
Outil de programmation littéraire
Project Leader : Christian QUEINNEC
Macao : Modélisation Analyse et Conception Assistées par Ordinateur
Macao est un logiciel générique de dessin de graphes. Avec une interface utilisateur intuitive, il permet de dessiner très facilement des graphes. Macao est aussi l'interface une interface utilisateur de FrameKit, une plate-forme dédiée au prototypage et à la validation de systèmes complexes.
Project Leader : Jean-Luc MOUNIER
09/1987
Système d'objets à la CLOS pour Scheme
Project Leader : Christian QUEINNEC
01/1993
PaInLeSS : Framework pour la parallélisation de solveurs SAT
Cet outil écrit en C++ simplifie l'implémentation et l'évaluation de nouveaux solveurs pour des environnements multi-coeurs. Les composants peuvent être instanciés indépendamment pour produire un nouveau solveur SAT .
Project Leader : Souheib Baarir
06/2019
PNML Framework est l'implémentation prototype du standard ISO/IEC-15909 (partie 2), le format d'échange normalisé pour les réseaux de Petri. L'objectif principal de PNML est d'aboutir à l'interopérabilité des outils basés sur les réseaux de Petri. PNML Framework est conçue pour implémenter le standard au fur et à mesure de son élaboration, afin d'en mesurer la faisabilité et de servir de référecne pour es outils de la communauté. Il propose une API de manipulation permettant de créer, sauver, charger et parcourir des réseaux de Petri au format PNML.
Project Leader : Fabrice KORDON
04/2005
Puck : Puck
Puck est un outil de refactoring de logiciels en Java qui détecte et casse les dépendances nuisibles. Les développeurs peuvent planifier leur refactoring sur un graphe de dépendances et l'appliquer à leur code automatiquement. Puck est encore un prototype de recherche.
Project Leader : Mikal ZIANE
10/2016
SPOT : Spot Produces Our Traces
SPOT (Spot Produces Our Traces) est une bibliothèque de model-checking facilement extensible. À la différence des model-checkers existants, dont le mode opératoire est immuable, SPOT fournit des briques que l'utilisateur peut combiner entre elles pour réaliser un model-checker répondant à ses propres besoins. Une telle modularité permet d'expérimenter facilement différentes combinaisons, et facilite le développement de nouveaux algorithmes. D'autre part, cette bibliothèque est centrée autour d'un type d'automates particulier permettant d'exprimer les propriétés à vérifier de façon plus compacte, qui n'a jamais été utilisé dans un outil jusqu'à présent.
Project Leader : Denis POITRENAUD
VBPMN : Framework pour la Vérification de processus BPMN
VBPMN supports formal modelling and automated analysis of business processes using formal verification tools. It features a web interface for comparing BPMN 2.0 models.
Project Leader : Pascal POIZAT
01/2016
VerChor : Framework pour la Vérification de Chorégraphies
VerChor enables you to design correct distributed systems following the choreography-based developement approach. Just model the system interaction protocol in your favorite language and let VerChor check for its realizability and retrieve peer interaction skeletons, or let it generate peer controllers to ensure the conformance to the system specification of a set of peers you want to reuse !
Project Leader : Pascal POIZAT
01/2013
