SUJET

ENCADREMENT : Nadjib Lazaar, Christian Bessiere

TITRE : Validation de contraintes globales en programmation par contraintes.

La programmation par contraintes (PPC) commence à être utilisée dans des applications critiques comme la gestion et le contrôle du trafic aérien ou le e-commerce. Dans ce cadre, les solutions développées doivent être validées avec le plus grand soin avant d’être utilisées de manière opérationnelle. Les théories de test existantes, dédiées aux programmes conventionnels, sont inopérantes pour capter les spécificités des programmes à contraintes. Il existe quelques travaux pionniers dans le domaine du test des programmes à contraintes (Lazaar et al. 2010, 2011, 2012), mais ils ne permettent pas de traiter un des apports majeurs de la programmation par contraintes à l’informatique : les contraintes globales.

Le sujet de thèse proposé s’inscrit dans ce contexte et vise à étendre le test de programmes à contraintes à la validation de contraintes globales. Le cadre de test existant fait appel à la réfutation : on cherche une solution d'un système A qui n'est pas une solution d’un système B. Cette approche est amenée à nier des contraintes globales. Nous devrons donc proposer une solution générique au problème de la négation des contraintes globales en nous inspirant des quelques travaux existants et proposer un cadre de test pour la validation de contraintes globales définies par des moyens génériques (automates, décompositions, etc.). Enfin, nous utiliserons l’apprentissage automatique pour faciliter la reformulation des contraintes et l’acquisition de contraintes (Bessiere et al., 2013) pour répondre au problème de l’oracle : tout processus de test exige la donnée d'une référence (un oracle) afin de déterminer la divergence entre une implantation et cette référence.

Les travaux proposés nécessitent des goûts (et aptitudes) pour la formalisation et raisonnement en contraintes (Programmation par contraintes), pour les formalismes existants en apprentissage automatique et en vérification des programmes, mais également pour la mise en œuvre, l’implémentation et l’expérimentation. Nous recherchons donc un candidat à l’aise avec les formalismes logiques, ayant des compétences en programmation en C++ et/ou en Java.

TITLE: Global constraints validation in constraint programming

The success of several constraint-based modeling languages appeals for better software engineering practices, particularly in the testing phase. These languages aim at solving industrial combinatorial problems that arise in optimization, planning, or scheduling. Recently, a new trend has emerged that proposes also to use CP programs to address critical applications in e-Commerce, air-traffic control and management, or critical software development that must be thoroughly verified before being used in applications. In previous works, we defined a first testing theory for constraint programming (Lazaar et al. 2010, 2011, 2012). We faced the problem of validating global constraints during their design and before their use. Global constraints represent one of the key successes of CP.

This phd thesis proposal falls within this context and aims at extending CP testing on the validation of global constraints. The present framework is based on a refutation-based approach. That is, find a solution of a system A that is not a solution of a system B. This approach can lead us to negate global constraints. We face the need to define a generic solution of global constraint negation problem based on a generic representation (DFA, MDD, decompositions…). Finally, we will use machine-learning techniques to ease the constraint reformulation and acquisition  (Bessiere et al., 2013) to address the oracle problem in CP testing.   

  • [Bessiere et al., 2013] C. Bessiere, R. Coletta, E. Hebrard, G. Katsirelos, N. Lazaar, N. Narodytska, C.G. Quimper, and T. Walsh. Constraint acquisition via partial queries. IJCAI'2013.
  • [Lazaar et al., 2012] N. Lazaar, A. Gotlieb, and Y. Lebbah. A CP framework for testing CP. Constraints Journal, 2012.
  • [Lazaar et al., 2011] N. Lazaar, A. Gotlieb, and Y. Lebbah. A framework for the automatic correction of constraint programs. ICST’2011.
  • [Lazaar et al., 2010] N. Lazaar, A. Gotlieb, and Y. Lebbah. Fault localization in constraint programs. ICTAI ’2010.

 

eXTReMe Tracker