OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Spécification formelle de systèmes temps réel répartis par une approche flots de données à contraintes temporelles

Le Berre, Tanguy. Spécification formelle de systèmes temps réel répartis par une approche flots de données à contraintes temporelles. PhD, Institut National Polytechnique de Toulouse, 2010

[img]
Preview
(Document in French)

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
1MB

Official URL: http://ethesis.inp-toulouse.fr/archive/00001141/

Abstract

Une définition des systèmes temps réel est que leur correction dépend de la correction fonctionnelle mais aussi du temps d'exécution des différentes opérations. Les propriétés temps réels sont alors exprimées comme des contraintes temporelles sur les opérations du système. Nous proposons dans cette thèse un autre point de vue où la correction est définie relativement à la validité temporelle des valeurs prises par les variables du système et aux flots de données qui parcourent le système. Pour définir ces conditions de validité, nous nous intéressons au rythme de mise à jour des variables mais aussi aux liens entre les valeurs des différentes variables du système. Une relation dite d'observation est utilisée pour modéliser les communications et les calculs du système qui définissent les liens entre les variables. Un ensemble de relations d'observation modélise l'architecture et les flots de données du système en décrivant les chemins de propagation des valeurs dans le système. Les propriétés temps réels sont alors exprimées comme des contraintes sur ces chemins de propagation permettant d'assurer la validité temporelle des valeurs prises par les variables. La validité temporelle d'une valeur est définie selon la validité temporelle des valeurs des autres variables dont elle dépend et selon le décalage temporel logique ou événementiel introduit par les communications ou les calculs le long des chemins de propagation. Afin de prouver la satisfiabilité d'une spécification définie par une telle architecture et de telles propriétés, nous construisons un système de transitions à état fini bisimilaire à la spécification. L'existence de ce système fini est justifiée par des bornes sur le décalage temporel entre les variables du système. Il est alors possible d'explorer les exécutions définies par ce système de transitions afin de prouver l'existence d'exécutions infinies satisfaisant la spécification.

Item Type:PhD Thesis
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut National Polytechnique de Toulouse - INPT
Laboratory name:
Research Director:
Padiou, Gérard and Quéinnec, Philippe
Statistics:download
Deposited By: admin admin
Deposited On:21 Nov 2012 13:06

Repository Staff Only: item control page