-
Selection by year
-
Selection by authors
-
Complete lists
stainer:tel-00926316
Amélie Stainer. Contribution à la vérification des automates temporisés : déterminisation, vérification quantitative et accessibilité dans les réseaux d'automates. PhD Thesis Université Rennes 1, November 2013.
Download [help]
Download paper:
Adobe portable document (pdf) 
Copyright notice:
This material is presented to ensure timely dissemination of scholarly and
technical work. Copyright and all rights therein are retained by authors or
by other copyright holders. All persons copying this information are expected
to adhere to the terms and constraints invoked by each author's
copyright. These works may not be reposted without the explicit permission of
the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic
Abstract
{Cette thèse porte sur la vérification des automates temporisés, un modèle bien établi pour les systèmes temps-réel. La thèse est constituée de trois parties. La première est dédiée à la déterminisation des automates temporisés, problème qui n'a pas de solution en général. Nous proposons une méthode approchée (sur-approximation, sous-approximation, mélange des deux) fondée sur la construction d'un jeu de sûreté. Cette méthode améliore les approches existantes en combinant leurs avantages respectifs. Nous appliquons ensuite cette méthode de déterminisation à la génération automatique de tests de conformité. Dans la seconde partie, nous prenons en compte des aspects quantitatifs des systèmes temps-réel grâce à une notion de fréquence des états acceptants dans une exécution d'un automate temporisé. Plus précisément, la fréquence d'une exécution est la proportion de temps passée dans les états acceptants. Nous nous intéressons alors à l'ensemble des fréquences des exécutions d'un automate temporisé pour étudier, par exemple, le vide de langages seuils. Nous montrons ainsi que les bornes de l'ensemble des fréquences sont calculables pour deux classes d'automates temporisés. D'une part, les bornes peuvent être calculées en espace logarithmique par une procédure non-déterministe dans les automates temporisés à une horloge. D'autre part, elles peuvent être calculées en espace polynomial dans les automates temporisés à plusieurs horloges ne contenant pas de cycles for{\c c}ant la convergence d'horloges. Finalement, nous étudions le problè me de l'accessibilité des états acceptants dans des réseaux d'automates temporisés qui communiquent via des files FIFO. Nous considérons tout d'abord des automates temporisés à temps discret, et caractérisons les topologies de réseaux pour lesquelles l'accessibilité est décidable. Cette caractérisation est ensuite étendue aux automates temporisés à temps continu.}
BibTex Reference
@PhdThesis{stainer:tel-00926316,
Author = {Stainer, Amélie},
Title = {{Contribution à la vérification des automates temporisés : déterminisation, vérification quantitative et accessibilité dans les réseaux d'automates}},
School = {Université Rennes 1},
Month = {November},
Year = {2013}
}
EndNote Reference [help]
Get EndNote Reference (.ref)