Projets-App
Projets
Editer un projet
Cadre de travail
Unité de recherche rattachée au CNRS
IRIF
LIPN
LMF
Information du ou de la responsable scientifique du projet :
Prénom
Nom
E-mail
Présentation du projet scientifique
Nom du project
Résumé publiable du projet (10 lignes max.)
Le PMC-SOG est un model-checker parallèle basé sur le graphe d'observation symbolique (SOG). Il reçoit en entrée un graphe de l'espace d'état d'un système et une propriété LTL et vérifie à la volée de manière parallèle et/ou distribuée si le système satisfait la propriété. Le PMC-SOG est implémenté en C++ et utilise la bibliothèque des threads de C++ et MPI.
Champs thématiques adressés (séparés par des virgules)
Type
proof-of-concept
prototype
maintenance/évolution logiciel existant
prématuration
Décrivez les innovations attendues à l'issue du projet (5 lignes max.)
Plusieurs techniques ont été utilisées pour atténuer le problème de l'explosion des états, notamment la réduction des ordres partiels (ROP). Par conséquent, l'intégration du ROP dans le PMC-SOG augmentera l'efficacité de l'outil, et permettra de vérifier des propriétés qui n'étaient pas possibles auparavant.
Argumentaire scientifique qui décrit le projet, l'état de l'art, les travaux antérieurs et les résultats attendus (20 lignes max.)
Le PMC-SOG est le résultat de plusieurs travaux de recherche au sein de l'équipe LoVe du LIPN (https://sites.lipn.univ-paris13.fr/websites/pmc-sog/). L'intégration de la réduction d'ordre partiel a été étudiée dans un sujet de stage de M2, mais de façon théorique uniquement.
Description du besoin en ingénierie
Évaluez le temps ingénieur dont vous avez besoin pour votre projet:
Frequence
2 jour/semaine
3 jour/semaine
Durée
1 mois
2 mois
3 mois
4 mois
5 mois
6 mois
Quelles sont les compétences spécifiques d'ingénierie attendues ; notamment, langages ou frameworks qui seront utilisés dans le projet, outils existants, connaissances requises ?
- Langage C++ - Programmation Orienté Objet - Notions de programmation parallèle
Décrivez les activités qui seront confiées à·aux ingénieur·e·s (si possible, avec un planning de tâches attendues)
- Implémentation de la réduction d'ordre partiel dans le PMC-SOG. - Écriture de tests unitaires et de régression. - Exécution des benchmarks pour comparer l'efficacité de la technique.
Commentaires
Mettre à jour