Modèles de temps pour la vérification des systèmes temps-réel
Actuellement, les méthodes formelles sont de plus en plus utilisées dans le but d'analyser le comportement les systèmes dits temps-réel.
Ces méthodes utilisent des modèles formels de spécification dotés de sémantiques bien définies et des techniques de vérification formelle.
D'autre part, les sémantiques de vrai parallélisme, comme la sémantique de maximalité, peuvent être utilisées à bon escient si on veut échapper à l'hypothèse de l'atomicité temporelle et structurelle des actions.
Des travaux antérieurs ont montré l'aptitude de modèles basés sur la maximalité, à l'image des systèmes de transitions étiquetées maximales, à supporter l'expression du parallélisme d'exécution d'actions.
Notre travail qui s'inscrit dans le cadre de la spécification et la vérification formelle des systèmes temps-réel consiste à tirer profit des avantages offerts par la sémantique de maximalité en l'appliquant à quelques modèles temporels et/ou temporisés.
Ainsi, nous proposons trois méthodes de génération de structures basés sur la maximalité (systèmes de transitions étiquetées maximales, DATA et DATA*) à partir de modèles de haut niveau.
Nabil Belala est actuellement un enseignant-chercheur en informatique à l'université Constantine 2 - Abdelhamid Mehri en Algérie.
Il a eu son diplôme de Magister en 2005 et son doctorat en 2010 de la même université.
Ses principaux domaines de recherche incluent la spécification et la vérification formelle des systèmes critiques.
Fiche technique
- Auteur
- Nabil Belala
- Langue
- Français
- Éditeur
- Éditions universitaires européennes
- Pays
- Algérie
30 autres produits dans la même catégorie :
Voir toutConception et réalisation d’une base de données pour la gestion
- Nouveau
Les Systèmes de Recommandation à Base de Filtrage Collaboratif
- Nouveau
Conception et réalisation d'une application de gestion des palmarès
- Nouveau
Mise en place d'un réseau informatique local avec connexion internet
- Nouveau
Répartition simultanée des nœuds dans un réseau de radio cognitive
- Nouveau
Vers une approche de monitoring des applications orientées services
- Nouveau
Le traitement des classes déséquilibrées par les méthodes ensemblistes
- Nouveau