Les systèmes temps réel (STR) sont au coeur de machines souvent jugés critiques pour la sécurité : ils en contrôlent l'exécution afin que celles-ci se comportent de manière sûre dans le contexte d'un environnement dont l'évolution peut être imprévisible. Un STR n'a d'autre alternative que de s'adapter `a son environnement : sa correction dépend des temps de réponses aux stimuli de ce dernier. Il est couramment admis que le formalisme des réseaux de Petri temporels (RdPT) est adapté à la description des STR. Cependant, la modélisation de systèmes simples, ne possédant que quelques tâches périodiques ordonnancées de façon basique se révèle être un exercice souvent complexe. En premier lieu, la modélisation efficace d'une gamme étendue de politiques d'ordonnancements se heurte à l'incapacité des RdPT à imposer un ordre d'apparition à des évènements concurrents survenant au même instant. D'autre part, les STR ont une nette tendance à être constitués de caract éristiques récurrentes, autorisant une modélisation par composants. Or les RdPT ne sont guère adaptés à une utilisation compositionnelle un tant soit peu générale. Afin de résoudre ces deux problèmes, nous proposons dans cette thèse Cifre - en partenariat entre Airbus et le Laas-Cnrs - d'étendre les RdPT à l'aide de deux nouvelles relations, les relations d'inhibition et de permission, permettant de spécifier de manière plus fine les contraintes de temps. Afin de cerner un périmètre clair d'adéquation de cette nouvelle extension à la modélisation des systèmes temps réel, nous avons défini Pola, un langage spécifique poursuivant deux objectifs : déterminer un sous-ensemble des systèmes temps réel modélisables par les réseaux de Petri temporels à inhibitions/permissions et fournir un langage simple à la communauté temps réel dont la vérification, idéalement automatique, est assurée par construction. Sa sémantique est donnée par traduction en réseaux de Petri temporels à inhibitions/permissions. L'explorateur d'espace d'états de la boite à outils Tina a été étendu afin de permettre la vérification des descriptions Pola.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00462521 |
| Date | 26 January 2010 |
| Creators | Peres, Florent |
| Publisher | INSA de Toulouse |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds