Assas Recherche | Un environnement de simulation pour la validation de spécifications B événementiel

Un environnement de simulation pour la validation de spécifications B événementiel (Document en Anglais)

Accès au(x) document(s)

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

http://docnum.univ-lorraine.fr/public/DDOC_T_2013_0158_YANG.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 : Yang Faqing

Yang, Faqing

Nom

Yang

Prénom

Faqing

Nationalité

Date de soutenance : 29-11-2013

Directeur(s) de thèse : Souquières Jeanine

Souquières, Jeanine

Nom

Souquières

Prénom

Jeanine

- Jacquot Jean-Pierre

Jacquot, Jean-Pierre

Nom

Jacquot

Prénom

Jean-Pierre

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 : Spécification, Vérification, Validation, Méthodes formelles, B événementiel, Simulation, JavaScript
Mots-clés :

B (méthode formelle)
Conception de systèmes informatiques
JavaScript (langage de programmation)
Logiciels -- Validation

Résumé : Cette thèse porte sur la spécification, la vérification et la validation de systèmes critiques à l'aide de méthodes formelles, en particulier, B événementiel. Nous avons travaillé sur l'utilisation de B événementiel pour étudier des algorithmes de contrôle du platooning, à partir d'une version 1D simplifiée vers une version 2D plus réaliste. L'analyse critique du modèle du platooning en 1D a découvert certaines anomalies. La difficulté d'exprimer les théorèmes de deadlock-freeness dans B événementiel nous a motivé pour développer un outil, le générateur de théorèmes de deadlock-freeness, pour construire automatiquement ces théorèmes. Notre évaluation a confirmé que les preuves mathématiques ne sont pas suffisantes pour vérifier la correction d'une spécification formelle : une spécification formelle doit aussi être validée. Nous pensons que les activités de validation, comme les activités de vérification, doivent être associées à chaque raffinement. Pour ce faire, nous avons besoin de meilleurs outils de validation. Certains outils d'exécution existants échouent pour certains modèles non-déterministes exprimés en B événementiel. Nous avons donc conçu et implanté un nouvel outil d'exécution, JeB, un environnement de simulation en JavaScript pour B événementiel. JeB permet aux utilisateurs d'insérer du code sûr à la main pour fournir des calculs déterministes lorsque la traduction automatique échoue. Pour atteindre cet objectif, nous avons défini des obligations de preuve qui garantissent la correction de simulations par rapport au modèle formel

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 : 2013LORR0158
Type de ressource : Thèse