" Soutenance de thèse de Vivien PELLETIER. | Université d'Orléans

Université d'Orléans

Soutenance de thèse de Vivien PELLETIER.

23/10/2017 - 10:00 - 23/10/2017 - 13:00

URL: http://www.univ-orleans.fr/actus/soutenances

Nom du contact: Etudes Doctorales

Courriel du contact: etudes.doctorales@univ-orleans.fr

Lieu: Amphi Herbrand - UFR Collegium d’ITP Sciences - Bâtiment 3IA - rue Léonard de Vinci - campus UNIVERSITÉ

Titre : Sur-approximations non régulières et terminaison pour l'analyse d'accessibilité.

Discipline : Informatique

ECOLE DOCTORALE MIPTIS

Résumé :

L'analyse d'accessibilité est une des composantes de l'analyse de modèles. Elle consiste à modéliser un système complexe par trois ensembles : le langage initial, le langage des configurations indésirables et un système de réécriture. Le langage initial et le langage des configurations indésirables sont des ensembles de termes. Un terme est un mot mais construit à partir de symboles d'arités supérieures à 1. Le système de réécriture représente la dynamique du système complexe. C'est un ensemble de règles qui permettent d'obtenir un nouveau terme à partir d'un terme original. Pour effectuer une analyse d'accessibilité à partir de cette modélisation, on peut calculer l'ensemble des configurations accessibles. Cet ensemble, aussi appelé ensemble des descendants, est obtenu en appliquant le système de réécriture sur le langage initial jusqu'à ne plus obtenir de nouveaux termes. Une fois l'ensemble des descendants calculé, il reste à faire l'intersection entre celui-ci et l'ensemble des configurations indésirables. Si cette intersection est vide, alors il n'y a pas de configuration indésirable accessible, sinon les configurations présentes dans cette intersection sont accessibles. Cependant, l'ensemble des descendants n'est pas calculable dans le cas général. Pour contourner ce problème, nous calculons une sur-approximation des descendants. Ainsi, si l'intersection est vide, cela signifie toujours qu'aucune configuration indésirable n'est accessible. A contrario, s'il existe un terme dans l'intersection, il n'est pas possible de déterminer s'il s'agit d'un faux positif ou d'une configuration indésirable accessible. La précision de la sur-approximation est alors déterminante. Nous proposons des résultats permettant d’améliorer la précision de ces sur-approximations en utilisant des classes de langages plus expressives.