Problèmes basés sur les Causes dans le cadre de la Logique Temporelle Linéaire: Théorie et Applications

La logique temporelle a traditionnellement été utilisée dans de nombreux champs de recherches comme la vérification de matériel, la synthèse, ou la représentation des connaissances. Récemment la logique temporelle a été appliquée à de nouveaux exemples d'applications comme les champs relevant des calculs orientés services, de la vérification /gestion de logiciel, la vérification de processus métier ou des systèmes de bases de données transactionnelles. Dans les champs des services, logiciels, processus métiers et bases de données, les méthodes agiles véhiculent de nouvelles questions de recherches. Les méthodes agiles sont orientées changements, évolutions et personnalisations pendant les étapes de conception ou de re-conception dans un style itératif. Elles adressent les problèmes de besoins (i.e., spécifications) qui évoluent. Ces changements/spécifications peuvent provenir de différents agents de manière non coordonnée ou non consistante. Un défi autour des méthodes agiles consiste à comprendre le système et ses spécifications dans le but de comprendre l'impact d'un changement (que peut-on garder, que peut-on enlever?). Les changements apparaissent le plus fréquemment lors de la désactivation d'une règle de conformité dans la spécification, l'ajout de règles, le retranchement de règles (désactivation puis ajout de règles). Du point de vue logique, les explications, l'inconsistance et les dépendances apparaissent fondamentales pour la gestion de méthodes agiles. Dans cette thèse, nous nous intéressons à la logique temporelle linéaire (LTL) avec une forte emphase sur la compréhension des systèmes et leurs spécifications, les causes logiques et explications. Nous proposons de revisiter quelques problèmes traditionnels de logique temporelle en considérant les explications, les causes et l'inconsistance. Nous proposons également d'approcher la notion d'implémentation d'une propriété/fonctionnalité: caractéristique à l'aide de la notion logique d'explication. Nos contributions se situent à trois niveaux : Au niveau théorique Nous proposons une classification des problèmes basés sur les causes en logique linéaire temporelle (CBP) (couverture, vacuité, interprétation abstraite, révisions, noyaux inconsistants minimaux, explications). Complexité : nous fournissons de nouveaux résultats concernant la complexité de calcul des CBP. Concernant les méthodes agiles Nous proposons une définition précise des explications et fragments de systèmes orientées données avec des artifacts métiers en tant que réponses à une requête LTL-FO représentant une règle de conformité. Nous proposons un encodage pour extraire toutes les explications Nous fournissons des résultats de complexité de calcul pour l'extraction de fragments. Nous fournissons une étude préliminaire concernant la notion de désactivation de règle et de couplage entre fragments dû à des erreurs d'implémentation. Au niveau Algorithmique: Nous proposons un algorithme préliminaire mais complet pour résoudre le problème de satisfiabilité de LTL. L'algorithme est fondé sur une recherche en profondeur avec une gestion des sous problèmes inconsistants. Il repose une fusion des algorithmes DPLL propositionnel, de la résolution pour la logique linéaire temporelle et de la recherche en profondeur dans un automate de Buchi