L?objectif du projet est d?explorer l?application de techniques de vérification de programme de type « software model checking » à la vérification automatique de règles métier – DECIDE

L'objectif de DECIDE ! est d'explorer l'application de techniques de vérification de programme de type « software model checking » à la vérification automatique de bases de règles métier. Il s'agit d'un projet exploratoire.
Plus les systèmes de gestion de règles métier se répandent dans les applications d'entreprise et plus ils sont présents dans des applications critiques, plus la pression augment sur les éditeurs de systèmes de gestion de règles métier (SGRM) pour qu'ils offrent des fonctions de validation des bases de règles. Ces fonctions sont inexistantes ou très limitées dans les produits leaders sur le marché des SGRM: ILOG JRules se contente, par exemple, si une incoherence dans les conditions d?une règle la rendent inapplicable. Par ailleurs, les produits de vérification de bases de règles commercialisés ne traitent pas le cas des règles de production. On peut donc considérer qu'il n'existe pas, à ce jour, sur le marché, de produit correspondant de près ou de loin au besoin auquel nous nous intéressons.
La question de la validation d?une base de règles a fait l'objet de nombreux travaux dans le domaine des systèmes experts. Ces travaux ne sont pas malheureusement pas applicables directement aux règles métier, de la forme si condition, alors action , dans lesquelles les actions sont des éléments de programme -dont l'exécution produit des effets de bords- et non des assertions logiques. Partant du constat que les règles métier sont, essentiellement, un outil de programmation orienté gestion de processus métier, on s'intéresse à l'application de techniques de vérification de programmes à la vérification de systèmes de règles métier.
DECIDE ! se situe évidemment au coeur de la priorité 2.1 : « Systèmes d?information d'entreprises et de groupes » du thème 2 (« Réseaux d'information et de connaissances »), à la croisée des problématiques de mise en oeuvre de règles métier -dans le cadre des architectures de services- et de validation de composants.
D'une manière générale, la vérification de programmes repose sur deux étapes : l'abstraction du programme à vérifier, puis la vérification que le programme abstrait possède certaines propriétés, elles-mêmes abstraites des propriétés souhaitées du programme à vérifier.
Dans ce projet, le verrou technologique réside dans les spécificités que les systèmes à base de règles métier représentent pour les algorithmes de raffinement automatique de l'abstraction dans la vérification de programmes : les règles sont exécutées sur un espace de données dynamique ; et pour les procédures de décisions : la richesse d'expression des langages de règles métier demandera d'étendre la procédure de décision pour SAT avec de nouvelles théories.
Du point de vue de la vérification de programmes, et de l'approche consistant à raffiner automatiquement l'abstraction du programme à vérifier, l'innovation tient d'une part dans l'application aux programmes à base de règles, d'autre part dans l'utilisation de procédures de décision dans le processus de raffinement. Du point de vue des procédures de décisions pour SAT, le sujet principal est l'extension pour la prise en compte d'autres théories. Les problèmes eux-mêmes sont NP-durs, ou pire.
Le deux partenaires sont ILOG (industriel) et Verimag (universitaire). ILOG est l'un des premiers fournisseurs mondiaux de composants logiciels d'entreprise et en particulier de SGRM. Verimag est une UMR de l'université J. Fournier, du CNRS et de l'Institut National Polytechnique de Grenoble.
ILOG pilotera le projet et apportera sa connaissance des SGRM (techniques, besoins, marché) et sa compétence en programmation par contraintes. Verimag apportera sa compétence et son expérience de la vérification de programme, et en particulier en ce qui concerne les procédures de décision.
Le projet est découpé en trois sous-projets : SP1 traite de l'abstraction des programmes à base de règles métier dans un but de vérification et SP2 développe des procédures de décision bas