Abstract FR:

Garantir la qualite du logiciel est presque banal en genie logiciel. Pour les systemes a base de connaissances, c'est moins habituel. Cette question n'a jusqu'ici pratiquement pas ete abordee pour des systemes de nouvelle generation bases sur un langage de tache. La base de connaissances comporte en plus des connaissances du domaine, une base de taches et de methodes. Pour des systemes flexibles deux autres composantes interviennent : une base de strategies et un meta-systeme de controle. Le travail presente dans cette these s'inscrit dans le cadre general de la garantie du logiciel pour de tels systemes. Pour des programmes classiques il est tout a fait naturel de s'assurer que les algorithmes utilises satisfont certaines bonnes proprietes. Nous nous sommes attaques a cette problematique pour des systemes a base de taches en choisissant de l'aborder au niveau de la semantique du langage. Le langage metatask, est un langage de programmation qui permet la realisation de systemes a base de taches flexibles, tout en garantissant les proprietes suivantes (i) la terminaison : le systeme s'arrete en un temps fini sur un echec ou sur un resultat, (ii) la correction : les resultats obtenus correspondent bien a des solutions aux problemes traites et (iii) la semi-completude : si une solution au probleme existe, elle sera obtenue par le systeme. Ces resultats reposent sur deux points cles. D'une part, la semantique des programmes ainsi que la dynamique des applications realisees sont rigoureusement definies grace a la specification formelle du langage, basee sur les types abstraits algebriques. D'autre part, nous avons sur-specifie le controle en imposant un noyau predefini pour le meta-controle. Ce noyau automatiquement ajoute a tout programme ecrit en metatask est lui-meme ecrit en metatask. Il permet la mise en uvre du principe de garde-fou qui, par la modification dynamique du controle en fonction du contexte de la resolution, evite des comportements indesirables.