Version accessible
  • fr
  • en
Recherche rapide
  • Aide
  • Recherche avancée
  • Nouveautés
Naviguer par :
  • Accueil
  • Mémoires
    • Nouveautés
      Recherche de nouveautés dans les ressources documentaires
    • Par master
      Recherche par master
    • Recherche avancée
      Recherche de ressources documentaires
    • Tous les mémoires
  • Thèses
    • Nouveautés
      Recherche de nouveautés dans les thèses
    • Recherche avancée
      Recherche de ressources
    • Par auteur
      Recherche par auteur
    • Par année
      Recherche par année de soutenance
    • Par laboratoire
      Recherche par laboratoire
    • Par thème
      Recherche thématique
    • Par école doctorale
      Recherche par école doctorale
    • Toutes les thèses
  • Publications de recherche
    • Nouveautés
      Recherche de nouveautés dans les ressources documentaires
    • Par laboratoire de recherche
      Recherche par laboratoire
    • Recherche avancée
      Recherche de publication de recherche
    • Toutes les publications de recherche
  • Tous les documents
    • Nouveautés
      Recherche des nouveautés
    • Recherche avancée
      Recherche avancée sur plusieurs formats
    • Toutes les ressources

Fiche descriptive

  • Vous êtes ici :
  • Accueil
  • »
  • Fiche descriptive
???menu.description..???
  • Imprimer
  • Version PDF
  • Version XML
  • Ajouter à ma sélection
  • Partager
  • Courriel
  • Twitter
  • Facebook
  • del.icio.us
  • BlogMarks
  • Viadeo
  • LinkedIn
Logiques de ressources dynamiques : modèles, propriétés et preuves (Document en Français)
Accès au(x) document(s)
Accéder au(x) document(s) :
  • http://docnum.univ-lorraine.fr/public/DDOC_T_2015_0033_COURTAULT.pdfLien brisé : nonDroits d'accès : non autorisé
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 : Courtault Jean-René
Courtault, Jean-René
Nom
Courtault
Prénom
Jean-René
Nationalité
Français

Date de soutenance : 15-04-2015

Directeur(s) de thèse : Galmiche Didier
Galmiche, Didier
Nom
Galmiche
Prénom
Didier


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 : Modélisation, Vérification et preuve, Logiques de ressources, Logiques de séparation, Dynamique, Méthodes des tableaux, Recherche de preuves, Méthodes formelles, Extraction de contre-Modèles
Mots-clés :
  • Logique informatique
  • Conception de systèmes informatiques
  • Systèmes dynamiques
  • Méthodes formelles (informatique)
  • Simulation, Méthodes de
Résumé : En informatique, la notion de ressource est une notion centrale. Nous considérons comme ressource toute entité pouvant être composée ou décomposée en sous-entités. Plusieurs logiques ont été proposées afin de modéliser et d’exprimer des propriétés sur celles-ci, comme la logique BI exprimant des propriétés de partage et de séparation. Puisque les systèmes informatiques manipulent des ressources, la proposition de nouveaux modèles capturant la dynamique de ces ressources, ainsi que la vérification et la preuve de propriétés sur ces modèles, sont des enjeux cruciaux. Dans ce contexte, nous définissons de nouvelles logiques permettant la modélisation logique de la dynamique des ressources, proposant de nouveaux modèles et permettant l’expression de nouvelles propriétés sur cette dynamique. De plus, pour ces logiques, nous proposons des méthodes des tableaux et d’extraction de contre-modèles. Dans un premier temps, nous définissons de nouveaux réseaux de Petri, nommés ß-PN, et proposons une nouvelle sémantique à base de ß-PN pour BI. Puis nous proposons une première extension modale de BI, nommée DBI, permettant la modélisation de ressources ayant des propriétés dynamiques, c’est-à-dire évoluant en fonction de l’état courant d’un système. Ensuite, nous proposons une logique, nommée DMBI, modélisant des systèmes manipulant/produisant/consommant des ressources. Par ailleurs, nous proposons une nouvelle logique (LSM) possédant de nouvelles modalités multiplicatives (en lien avec les ressources). Pour finir, nous introduisons la séparation au sein des logiques épistémiques, obtenant ainsi une nouvelle logique ESL, exprimant de nouvelles propriétés épistémiques
  
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 : 2015LORR0033
Type de ressource : Thèse
À propos Aide
ORI-OAI-search 2.0.7 - © 2006-2014 ORI-OAI