Assas Recherche | Un cadre formel pour l'intégration de connaissances du domaine dans la conception des systèmes : application au formalisme Event-B

Un cadre formel pour l'intégration de connaissances du domaine dans la conception des systèmes : application au formalisme Event-B (Document en Français)

Accès au(x) document(s)

Accéder au(x) document(s) :

http://docnum.univ-lorraine.fr/public/DDOC_T_2018_0230_KHERROUBI.pdf

Ce document est protégé en vertu du Code de la Propriété Intellectuelle.

Modalités de diffusion de la thèse :

Thèse consultable sur internet, en texte intégral.

Informations sur les contributeurs

Auteur : Kherroubi Souad

Kherroubi, Souad

Nom

Kherroubi

Prénom

Souad

Nationalité

Français

Date de soutenance : 21-12-2018

Directeur(s) de thèse : Méry Dominique

Méry, Dominique

Nom

Méry

Prénom

Dominique

Etablissement de soutenance : Université de Lorraine

Université de Lorraine

Nom

Université de Lorraine

Laboratoire : Laboratoire lorrain de recherche en informatique et ses applications

Laboratoire lorrain de recherche en informatique et ses applications

Nom

Laboratoire lorrain de recherche en informatique et ses applications

Ecole doctorale : École doctorale IAEM Lorraine - Informatique, Automatique, Électronique - Électrotechnique, Mathématiques de Lorraine (1992-....)

École doctorale IAEM Lorraine - Informatique, Automatique, Électronique - Électrotechnique, Mathématiques de Lorraine (1992-....)

Nom

École doctorale IAEM Lorraine - Informatique, Automatique, Électronique - Électrotechnique, Mathématiques de Lorraine (1992-....)

Informations générales

Discipline : Informatique
Classification : Informatique

Mots-clés libres : Méthodes formelles, Preuve, Modélisation, Représentation des connaissances, Raisonnement ontologique, Formalismes logiques, Event-B, Raffinement
Mots-clés :

Méthodes formelles (informatique)
B (méthode formelle)
Représentation des connaissances
Ontologies (informatique)
Conception de systèmes informatiques

Résumé : Cette thèse vise à définir des techniques pour mieux exploiter les connaissances du domaine dans l’objectif de rendre compte de la réalité de systèmes qualifiés de complexes et critiques. La modélisation est une étape indispensable pour effectuer des vérifications et exprimer des propriétés qu’un système doit satisfaire. La modélisation est une représentation simplificatrice, mais réductionniste de la réalité d’un système. Or, un système complexe ne peut se réduire à un modèle. Un modèle doit s’intégrer dans sa théorie observationnelle pour rendre compte des anomalies qu’il peut y contenir. Notre étude montre clairement que le contexte est la première problématique à traiter car principale source de conflits dans le processus de conception d’un système. L’approche retenue dans cette thèse est celle d’intégrer des connaissances du domaine en associant le système à concevoir à des formalismes déclaratifs qualifiés de descriptifs appelés ontologies. Notre attention est portée au formalisme Event-B dont l’approche correct-par-construction appelée raffinement est le principal mécanisme dans ce formalisme qui permet de faire des preuves sur des représentations abstraites de systèmes pour exprimer/vérifier des propriétés de sûreté et d’invariance. Le premier problème traité concerne la représentation et la modélisation des connaissances du contexte en V&V de modèles. Suite à l’étude des sources de conflits, nous avons établi de nouvelles règles pour une extraction de connaissances liées au contexte par raffinement pour la V&V. Une étude des formalismes de représentation et d’interprétation logiques du contexte a permis de définir un nouveau mécanisme pour mieux structurer les modèles Event-B. Une deuxième étude concerne l’apport des connaissances du domaine pour la V&V. Nous définissons une logique pour le formalisme Event-B avec contraintes du domaine fondées sur les logiques de description, établissons des règles à exploiter pour l’intégration de ces connaissances à des fins de V&V. L’évaluation des propositions faites portent sur des études de cas très complexes telles que les systèmes de vote dont des patrons de conception sont aussi développés dans cette thèse. Nous soulevons des problématiques fondamentales sur la complémentarité que peut avoir l’intégration par raffinement des connaissances du domaine à des modèles en exploitant les raisonnements ontologiques, proposons de définir de nouvelles structures pour une extraction partiellement automatisée

Informations techniques

Type de contenu : Text
Format : PDF

Informations complémentaires

Entrepôt d'origine :

STAR : dépôt national des thèses électroniques françaises

Identifiant : 2018LORR0230
Type de ressource : Thèse