Une Approche par Décomposition de Modèles pour l'Analyse de la Diagnosticabilité des SEDs par Model-Checking

Résumé : Cet article s'intéresse à la vérification de la diagnosticabilité des systèmes à évènements discrets (SEDs) dans le contexte de model-checking. Le formalisme de modélisation adopté est les systèmes de transitions labellisés (LTSs). Dans un premier lieu, nous proposons un algorithme permettant la transformation d’un LTS à base d'évènements en un LTS à base d'états, dont le but est d'étendre l'application de l'analyse de la diagnosticabilité par Model-Checking au contexte de diagnostic à base d'évènements. Pour remédier au problème de l'explosion combinatoire de l'espace d'états, nous proposons une technique de décomposition de modèles, qui permet d'extraire uniquement la partie nécessaire pour l'analyse de la diagnosticabilité. L'idée est basée sur la séparation entre les comportements normal et fautif du système. Dans le cas où le système est diagnosticable, nous fournissons une spécification dans la logique temporelle RT-CTL pour analyser la Kmin-diagnosticabilité en un coup, sans faire appel à un processus incrémental. L'évaluation de nos contributions est faite à travers une étude expérimentale effectuée sur un benchmark relatif à un système de contrôle/commande ferroviaire.
Type de document :
Communication dans un congrès
Stephan Merz and Jean-François Pétin. Modélisation des Systèmes Réactifs (MSR 2015), Nov 2015, Nancy, France
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01224281
Contributeur : Stephan Merz <>
Soumis le : mercredi 4 novembre 2015 - 14:45:03
Dernière modification le : jeudi 15 mars 2018 - 14:28:06
Document(s) archivé(s) le : vendredi 5 février 2016 - 11:30:52

Fichier

paper 13.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01224281, version 1

Collections

Citation

Abderraouf Boussif, Mohamed Ghazel. Une Approche par Décomposition de Modèles pour l'Analyse de la Diagnosticabilité des SEDs par Model-Checking. Stephan Merz and Jean-François Pétin. Modélisation des Systèmes Réactifs (MSR 2015), Nov 2015, Nancy, France. 〈hal-01224281〉

Partager

Métriques

Consultations de la notice

165

Téléchargements de fichiers

114