Méthodologie et outil de Test, de localisation de fautes et de correction automatique des programmes à contraintes
Institution:
Rennes 1Disciplines:
Directors:
Abstract EN:
The success of several constraint-based modelling languages such as OPL (Optimization programming Language) of IBM Ilog, COMET of Dynadec, Sicstus Prolog, Gecode, 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 propose 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. While constraint program debugging drew the attention of many researchers, few supports in terms of software engineering and testing have been proposed to help verify this kind of programs. In the present thesis, we define a testing theory for constraint programming. For that, we propose a general framework of constraint program development which supposes that a first declarative and simple constraint model is available from the problem specifications analysis. Then, this model is refined using classical techniques such as constraint reformulation, surrogate, redundant, implied and global constraint addition, or symmetry-breaking to form an improved constraint model that must be tested before being used to address real-sized problems. We think that most of the faults are introduced in this refinement step and propose a process which takes the first declarative model as an oracle for detecting non-conformities and derive practical test purposes from this process. Therefore, we enhance the proposed testing framework to introduce a methodology for an automatic tuning with fault localization and correction in constraint programs. We implemented these approaches in a new tool called CPTEST that was used to automatically detect, localize and correct faults on classical benchmark programs and real-world CP problem: the car-sequencing problem.
Abstract FR:
Le développement des langages de modélisation des programmes à contraintes a eu un grand impact dans le monde industriel. Des langages comme OPL (Optimization Programming Language) de IBM Ilog, Comet de Dynadec, Sicstus Prolog, Gecode, ainsi que d'autres, proposent des solutions robustes aux problèmes du monde réel. De plus, ces langages commencent à être utilisés dans des applications critiques comme la gestion et le contrôle du trafic aérien, le e-commerce et le développement de programmes critiques. D'autre part, il est connu que tout processus de développement logiciel effectué dans un cadre industriel inclut impérativement une phase de test, de vérification formelle et/ou de validation. Par ailleurs, les langages de programmation par contraintes (PPC) ne connaissent pas d'innovations majeures en termes de vérification et de mise au point. Ceci ouvre la voie à des recherches orientées vers les aspects génie logiciel dédiés à la PPC. Notre travail vise à poser les jalons d'une théorie du test des programmes à contraintes pour fournir des outils conceptuels et des outils pratiques d'aide à cette vérification. Notre approche repose sur des hypothèses quant au développement et au raffinement dans un langage de PPC. Il est usuel de démarrer à partir d'un modèle simple et très déclaratif, une traduction fidèle de la spécification du problème, sans accorder un intérêt à ses performances. Par la suite, ce modèle est raffiné par l'introduction de contraintes redondantes ou reformulées, l'utilisation de structures de données optimisées, de contraintes globales, de contraintes qui cassent les symétries, etc. Nous pensons que l'essentiel des fautes introduites est compris dans ce processus de raffinement. Le travail majeur présenté dans la présente thèse est la définition d'un cadre de test qui établit des règles de conformité entre le modèle initial déclaratif et le programme optimisé dédié à la résolution d'instances de grande taille. Par la suite, nous proposons un cadre conceptuel pour la mise-au-point de ce type de programmes avec une méthodologie pour la localisation et la correction automatique des fautes. Nous avons développé un environnement de test, nommé CPTEST, pour valider les solutions proposées, sur des problèmes académiques du monde de la PPC ainsi qu'un problème du monde réel qui est le problème d'ordonnancement des véhicules.