Approximation de relations de transition : application à la vérification de systèmes infinis - Université de Lorraine Accéder directement au contenu
Thèse Année : 2003

Approximation de relations de transition : application à la vérification de systèmes infinis

Résumé

Non disponible/Not available
Les systèmes de transition sont utilisés pour modéliser des systèmes informatiques complexes. Leurs spécifications, décrites avec la logique temporelle, peuvent être vérifiées en utilisant des algorithmes de vérification de modèles basés sur des calculs itératifs de plus petits et plus grands points fixes de fonctions sur les ensembles d'états. La représentations symbolique des ces ensembles permet d'étudier des systèmes avec un nombre infini d'états mais la terminaison des algorithmes de vérification de modèles n'est plus assurée. Plusieurs approches reposant sur un renforcement des spécifications requises permettent d'accélérer ou de forcer cette terminaison. Nous étudions ici des systèmes affines définis par morceaux. Notre but est de proposer des ensembles d'états stables par le système, permettant de calculer un nombre infini de transitions en une étape de calcul symbolique. Dans un premier temps, nous présenterons des approximations par des formules polynomiales. Ensuite, nous donnerons des formules d'approximation linéaires. Enfin, nous illustrerons notre approche par quelques exemples.

Domaines

Autre [cs.OH]
Fichier non déposé

Dates et versions

tel-01746595 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01746595 , version 1

Accès intranet

Citer

Julien Musset. Approximation de relations de transition : application à la vérification de systèmes infinis. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2003. Français. ⟨NNT : 2003NAN10229⟩. ⟨tel-01746595⟩
13 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More