Forge
MoVe Software
BCM4Java : Basic Component Model for Java
This project is an implementation of a distributed software component model in Java (20.000 lines of code and documentation today, under GitHub). It proposes the main concepts of the component-based approach: software components, component interface, ports exposing interfaces required and offered by components and explicit connectors. Using the Java RMI technology, it enables distributed programming thanks to de the deployment of components on several Java virtual machines (executing on several computers) and to calls between components through RMI. Started in the context of the ANR SALTY research project where it allowed to implement an application deploying 10.000 distributed components, this software has been used by several hundreds of students and is still being used first in the context of the ALASCA master 2 course since 2014 and in the context of the Components master 1 course since 2019.
Project Leader : Jacques MALENFANT
11/2012
BCMCyPhy : Component model for cyber-physical control systems
This research project and its associated software aim at designing and implementing a software component model for cyber-physical control systems. It develops over the BCM4Java project from which it uses the basic concepts and the implementation of distributed components in Java (10.000 lines of code and documentation today). Besides integrating real time components, this project studies component-based software architectures for control, their specification using stochastic hybrid systems and their simulation using models following the DEVS standard. A particular focus is given on the parallel composability between components, their individual specifications and simulation models. A software subproject of BCMCyPhy proposes a new implementation in Java of the DEVS standard for modular simulation of components and their assemblies (20.000 lines of code and documentation today). The simulators obtained through the composition of the components simulator models allow to debug, test, verify and validate applications. This software has been used by a few tens of students and is still being used in the context of the ALASCA master 2 course since 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 : Symmetry controller
Cosy is an efficient C++ library designed to dynamically break symmetries in SAT solving. It builds upon state-of-the-art SAT solvers by integrating a symmetry controller that works in tandem with the Conflict-Driven Clause Learning (CDCL) algorithm. Cosy can be interfaced with most CDCL solvers, offering flexibility and improved performance, especially in highly symmetric SAT problem instances. It is available under an open-source GPL v3 license.
Project Leader : Souheib Baarir
04/2018
CosyVerif : Software Environment for the Formal Specification and Verification of Dynamic Systems
CosyVerif is a software environment whose goal is the formal specification and verification of dynamic systems.
Project Leader : Fabrice KORDON
06/2019
is a Petri Net based CASE environment. It offers a set of services to perform specification, validation, formal verification, model checking, compute structural properties (invariants, traps, syphons etc.) simulate and generate code. These services have been implemented either by members of our team or university partners (Technical university of Helsinki, University of Torino, Technical university of Munchen, Bell laboratories). The second geration of CPN-AMI, build on top of FrameKit, is available on the Internet since March 1997.
Project Leader : Fabrice KORDON
12/1994
DDD : Library for manipulation of Data Decision Diagrams
libDDD is a package for manipulation of Data Decision Diagrams and Hierarchical Set Decision Diagrams. It supports flexible data types and "saturation" algorithms to offer cutting edge performances using decision diagrams. It is a C++ package distributed under Gnu LGPL.
Project Leader : Yann THIERRY-MIEG
01/2001
ITS-Tools : Instantiable Transition System Tools
ITS-tools is an easy to use and powerful award-winning model-checker supporting Safety, CTL and LTL properties for a variety of formalisms. It formally proves system correctness using exhaustive state space exploration.
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 is a generic graph drawing software that lets you create and manipulate graphs quickly and easily. It is an intuitive interface that enables to automates many of the time-consuming tasks involved in building graphs. Macao customization facilities enable the quick implementation of a new graph editor dedicated to a new type of graphical representation.This enable prototyping of new formalism, which is usefull when defining them. Macao can be considered as a standalone tool. However, it is a natural complement to FrameKit, a software platform dedicated to the prototyping and quick implementation of CASE environments.
Project Leader : Jean-Luc MOUNIER
09/1987
Meroon is an Object-Oriented System written in Scheme.
Project Leader : Christian QUEINNEC
01/1993
PaInLeSS : PArallel INstantiabLE Sat Solver
PArallel INstantiabLE Sat Solver (Painless) is a framework written in C++ that simplifies the implementation and evaluation of new parallel SAT solvers for many-core environments. The components of Painless can be instantiated independently to produce a new complete solver. The guiding principle is to separate the technical components dedicated to some specific aspect of concurrent programming, from the components implementing heuristics and optimizations embedded in a parallel SAT solver.
Project Leader : Souheib Baarir
06/2019
PNML Framework is a prototype implementation of ISO/IEC-15909 part 2, International Standard on Petri Net Markup Language. The primary purpose of PNML is to enable interoperability among Petri net tools. PNML framework has thus been designed to back the Standard. It will enable Petri nets tools developers to seamlessly integrate PNML support into their tools. It provides an extensive and comprehensible API to create, save, load and browse PNML models.
Project Leader : Fabrice KORDON
04/2005
Puck : Puck
Puck is an architecture refatoring tool for Java software, which allows developpers to detect and remove unwanted dependencies from code.They can plan their refactorings on dependency graphs and then apply their plans to code automatically. Puck is still a research prototype.
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 for the Verification of BPMN processes
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 for the Verification of Choreographies
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
