Main.Recherche History

Hide minor edits - Show changes to output

26/01/2009 16:02 by 134.214.106.53 -
Changed lines 6-7 from:
%color=blue% Manuscrit: ([[Attach:TheseBenHedia.pdf|ici]])
to:
%color=blue% Manuscrit: ([[Attach:TheseBenHedia.pdf|ici]])\\
26/01/2009 16:02 by 134.214.106.53 -
Added lines 6-10:
%color=blue% Manuscrit: ([[Attach:TheseBenHedia.pdf|ici]])

%color=blue% Présentation: ([[Attach:TalkTheseBenHedia.pdf|ici]])

31/12/2008 21:18 by 82.235.44.69 -
Changed lines 3-5 from:
%color=blue define=Analyse% '''Analyse temporelle des systèmes d’acquisition de données : une approche à base d’automates temporisés communicants et d’observateurs.'''

to:
%color=blue define=Analyse % '''Analyse temporelle des systèmes d’acquisition de données : une approche à base d’automates temporisés communicants et d’observateurs.'''

Changed line 28 from:
Dans le cadre de mes activités de recherche, je m’intéresse à la validation temporelle des applications temps réel. Dans mes travaux de thèse, nous avons défini une méthodologie d’évaluation des propriétés temporelles (par exemple les délais d’acheminement d’une donnée) des pilotes d’équipement des applications temps réel embarquées. Enfin, j’ai eu l’occasion, au cours de mes recherches, de m’intéresser aux environnements de spécification, conception, modélisation et validation des applications temps réel tels que l’outil IF, les automates temporisés communicants, la boîte à outil CADP.
to:
%justify% Dans le cadre de mes activités de recherche, je m’intéresse à la validation temporelle des applications temps réel. Dans mes travaux de thèse, nous avons défini une méthodologie d’évaluation des propriétés temporelles (par exemple les délais d’acheminement d’une donnée) des pilotes d’équipement des applications temps réel embarquées. Enfin, j’ai eu l’occasion, au cours de mes recherches, de m’intéresser aux environnements de spécification, conception, modélisation et validation des applications temps réel tels que l’outil IF, les automates temporisés communicants, la boîte à outil CADP.
Changed lines 31-33 from:
Les systèmes de contrôle de processus, c’est-à-dire les systèmes en charge du suivi et/ou du contrôle d’un processus physique auquel ils sont liés, sont présents dans des nombreux secteurs d’activités (système de contrôle de production, ferroviaire, avionique, spatiale ou encore domotique). Ces systèmes informatiques dont le comportement dépend de l’évolution du processus qu’ils contrôlent sont critiques: une défaillance du contrôle peut avoir des conséquences catastrophiques.

Les systèmes de contrôle de processus sont des systèmes réactifs qui contrôlent en temps réel leur environnement physique. Du fait de l’évolution dynamique du processus, les systèmes de contrôle commandent le processus en fonction des “ informations ” ou des données mesurées sur ce dernier et traduisant son évolution, dans un temps contraint pour assurer un contrôle correct.
to:
%justify% Les systèmes de contrôle de processus, c’est-à-dire les systèmes en charge du suivi et/ou du contrôle d’un processus physique auquel ils sont liés, sont présents dans des nombreux secteurs d’activités (système de contrôle de production, ferroviaire, avionique, spatiale ou encore domotique). Ces systèmes informatiques dont le comportement dépend de l’évolution du processus qu’ils contrôlent sont critiques: une défaillance du contrôle peut avoir des conséquences catastrophiques.

%justify% Les systèmes de contrôle de processus sont des systèmes réactifs qui contrôlent en temps réel leur environnement physique. Du fait de l’évolution dynamique du processus, les systèmes de contrôle commandent le processus en fonction des “ informations ” ou des données mesurées sur ce dernier et traduisant son évolution, dans un temps contraint pour assurer un contrôle correct.
Changed lines 36-37 from:
En effet, le système de contrôle évolue, non seulement en fonction des valeurs des informations “ en entrée ”, mais aussi en fonction de leur qualité d’acquisition (précision, retard,...).
to:
%justify% En effet, le système de contrôle évolue, non seulement en fonction des valeurs des informations “ en entrée ”, mais aussi en fonction de leur qualité d’acquisition (précision, retard,...).
Changed lines 39-40 from:
Ce flot d’informations en “entrée” d’un système de contrôle de processus est construit par un ensemble de composants de mesure appelés “ capteurs ”, et à destination de l’application de contrôle. De plus, les systèmes de contrôle de processus intègrent un (ou plusieurs) composant logiciel appelé “ pilote d’équipement ” permettant de fournir une interface entre l’application et l’équipement (ici le ou les capteurs). Le pilote d’équipement est un composant logiciel qui affecte d’une manière importante la qualité des informations transmises à l’application de contrôle et donc la qualité des systèmes. Le pilote de capteur ou pilote d’acquisition est un composant critique du système, il est à l’origine de plusieurs bugs et crashs des systèmes de contrôle de processus.
to:
%justify% Ce flot d’informations en “entrée” d’un système de contrôle de processus est construit par un ensemble de composants de mesure appelés “ capteurs ”, et à destination de l’application de contrôle. De plus, les systèmes de contrôle de processus intègrent un (ou plusieurs) composant logiciel appelé “ pilote d’équipement ” permettant de fournir une interface entre l’application et l’équipement (ici le ou les capteurs). Le pilote d’équipement est un composant logiciel qui affecte d’une manière importante la qualité des informations transmises à l’application de contrôle et donc la qualité des systèmes. Le pilote de capteur ou pilote d’acquisition est un composant critique du système, il est à l’origine de plusieurs bugs et crashs des systèmes de contrôle de processus.
Changed lines 42-43 from:
La validation des propriétés temporelles des systèmes de contrôle de processus se base sur une connaissance des caractéristiques temporelles des flots d’informations en “ entrée ” du système de contrôle. La caractérisation de flots d’information acheminés à partir des capteurs à l’application de contrôle se traduit par une évaluation des caractéristiques temporelles de cette la chaîne d’acquisition. Vu le contexte temps réel des systèmes de contrôle de processus cette validation se doit d’être exhaustive et formelle.
to:
%justify% La validation des propriétés temporelles des systèmes de contrôle de processus se base sur une connaissance des caractéristiques temporelles des flots d’informations en “ entrée ” du système de contrôle. La caractérisation de flots d’information acheminés à partir des capteurs à l’application de contrôle se traduit par une évaluation des caractéristiques temporelles de cette la chaîne d’acquisition. Vu le contexte temps réel des systèmes de contrôle de processus cette validation se doit d’être exhaustive et formelle.
Changed lines 45-60 from:
J’ai débuté mon travail de recherche par un travail de modélisation des systèmes d’acquisition des données. J’ai étudié la sémantique des automates temporisés communicants dans IF, l’instrumentation de modèle pour extraire les propriétés temporelles cherchées. Ceci m’a permis de donner dans MSR 05 [1] et FDL 05 [2] des résultats d’évaluation des propriétés temporelles (par exemple le retard) sur des exemples complexes et réalistes et une comparaison avec des résultats obtenus avec une méthode analytique basée sur l’ordonnancement. Ceci a permis de montrer l’intérêt d’une modélisation à l’aide des automates temporisés et l’analyse exhaustive des modèles. Les résultats obtenus présentes des détails qu’on ne trouve pas à l’aide d’une approche analytique qui ne donne que des bornes. La possibilité de prendre en compte une modélisation des temps de traitements variables (liés à une analyse d’ordonnancement) et ainsi de faire le lien entre les pilotes d’équipements, la politique d’ordonnancement et le choix des paramètres (priorité des tâches), nous a permis d’étudier des exemples beaucoup plus réalistes et beaucoup plus complexes.

La validation des propriétés temporelles des pilotes des systèmes d’acquisition pour le contrôle de processus s’effectue alors en plusieurs étapes:
* Identifier les propriétés temporelles à vérifier pour le système d’aquisition vis-à-vis du système de contrôle.
* Modéliser le système et son pilote d’équipement.
* Choisir un langage (et outils associés) pour la formalisation des modèles.
* Analyser et vérifier des propriétés.
* Paramétrer le pilote d’équipement et le système de contrôle en fonction des résultats trouvé lors des étapes précédentes.

Nous avons commencé par la suite plusieurs travaux afin de résoudre quelques problèmes :
* Définir mathématiquement les propriétés des QoS à vérifier à l’aide de logique temps réel (RTL).
* L’utilisation des automates observateurs pour récupérer les mesures souhaitées afin de résoudre les problèmes de l’explosion combinatoire que l’on a rencontré.
* Le développement d’un pilote d’équipement sous linux temps réel (RTAI) (travail effectué dans le cadre d’un projet de fin d’étude DUT), puis sous VxWorks afin d’avoir des résultats réels pour les comparer avec les résultats trouvés avec IF (les premiers résultats sont très proches de ceux calculés avec IF). Ce travail a permis aussi d’avoir des traces de mesures de performance qu’on utilisera afin de donner une caractérisation stochastique de notre modèle.
* L’utilisation de temps continu pour la simulation IF à la place de temps discret utilisé jusqu’à présent.

Depuis le début de la thèse l’approche utilisée était de proposer un modèle de système d’acquisition (spécialement de pilote d’équipement) puis d’instrumenter ce modèle afin d’évaluer les propriétés de QoS. Après avoir développé un pilote d’équipement et afin d’avoir des modèles plus réalistes, j’ai modifié mon approche, la nouvelle approche propose un modèle de pilote d’équipement basé sur les architectures logiciels des implémentations des pilotes d’équipement (implémentation réalisée sous VxWorks). Cette approche m’a permis d’avoir un modèle plus réaliste, l’observation de ce modèle à l’aide des observateurs (un observateur pour chaque propriété à évaluer) a permis d’avoir une évaluation de la QoS en fonction des paramètres du pilote d’équipement.
to:
%justify% J’ai débuté mon travail de recherche par un travail de modélisation des systèmes d’acquisition des données. J’ai étudié la sémantique des automates temporisés communicants dans IF, l’instrumentation de modèle pour extraire les propriétés temporelles cherchées. Ceci m’a permis de donner dans MSR 05 [1] et FDL 05 [2] des résultats d’évaluation des propriétés temporelles (par exemple le retard) sur des exemples complexes et réalistes et une comparaison avec des résultats obtenus avec une méthode analytique basée sur l’ordonnancement. Ceci a permis de montrer l’intérêt d’une modélisation à l’aide des automates temporisés et l’analyse exhaustive des modèles. Les résultats obtenus présentes des détails qu’on ne trouve pas à l’aide d’une approche analytique qui ne donne que des bornes. La possibilité de prendre en compte une modélisation des temps de traitements variables (liés à une analyse d’ordonnancement) et ainsi de faire le lien entre les pilotes d’équipements, la politique d’ordonnancement et le choix des paramètres (priorité des tâches), nous a permis d’étudier des exemples beaucoup plus réalistes et beaucoup plus complexes.

%justify% La validation des propriétés temporelles des pilotes des systèmes d’acquisition pour le contrôle de processus s’effectue alors en plusieurs étapes:
* %justify% Identifier les propriétés temporelles à vérifier pour le système d’aquisition vis-à-vis du système de contrôle.
* %justify% Modéliser le système et son pilote d’équipement.
* %justify% Choisir un langage (et outils associés) pour la formalisation des modèles.
* %justify% Analyser et vérifier des propriétés.
* %justify% Paramétrer le pilote d’équipement et le système de contrôle en fonction des résultats trouvé lors des étapes précédentes.

%justify% Nous avons commencé par la suite plusieurs travaux afin de résoudre quelques problèmes :
* %justify% Définir mathématiquement les propriétés des QoS à vérifier à l’aide de logique temps réel (RTL).
* %justify% L’utilisation des automates observateurs pour récupérer les mesures souhaitées afin de résoudre les problèmes de l’explosion combinatoire que l’on a rencontré.
* %justify% Le développement d’un pilote d’équipement sous linux temps réel (RTAI) (travail effectué dans le cadre d’un projet de fin d’étude DUT), puis sous VxWorks afin d’avoir des résultats réels pour les comparer avec les résultats trouvés avec IF (les premiers résultats sont très proches de ceux calculés avec IF). Ce travail a permis aussi d’avoir des traces de mesures de performance qu’on utilisera afin de donner une caractérisation stochastique de notre modèle.
* %justify% L’utilisation de temps continu pour la simulation IF à la place de temps discret utilisé jusqu’à présent.

%justify% Depuis le début de la thèse l’approche utilisée était de proposer un modèle de système d’acquisition (spécialement de pilote d’équipement) puis d’instrumenter ce modèle afin d’évaluer les propriétés de QoS. Après avoir développé un pilote d’équipement et afin d’avoir des modèles plus réalistes, j’ai modifié mon approche, la nouvelle approche propose un modèle de pilote d’équipement basé sur les architectures logiciels des implémentations des pilotes d’équipement (implémentation réalisée sous VxWorks). Cette approche m’a permis d’avoir un modèle plus réaliste, l’observation de ce modèle à l’aide des observateurs (un observateur pour chaque propriété à évaluer) a permis d’avoir une évaluation de la QoS en fonction des paramètres du pilote d’équipement.
Changed lines 63-71 from:
Mes traveaux de recherche propose une approche pour l’évaluation formelle des caractéristiques temporelles des chaines d’acquisition de données dans les systèmes de contrôle de processus. Cette évaluation est basée sur les automates temporisés communicants et les observateurs de propriétés.

Les résultats obtenus dans ce travail se focalisent sur plusieurs aspects.
Le premier point consiste en la mise
en place de l’instrumentation d’un observateur d’occurrence pour l’évaluation des propriétés temporelles. L’évaluation des caractéristiques temporelles des occurrences d’un flot de données d’une chaîne d’acquisition nécessite la formalisation du comportement du cycle de vie d’une occurrence de donnée dans une chaîne d’acquisition (production et consommation de l’occurrence, création et suppression de copie, fin de vie de l’occurrence). L’observation des occurrences est orientée pour l’évaluation du “ retard ”.

Le deuxième point consiste en la modélisation du système, en particulier le pilote d’équipement, et en l’évaluation et la caractérisation fine des propriétés temporelles des retards. La modélisation de la chaine d’acquisition est présentée sous la forme de deux approches de modélisation de la chaîne d’acquisition et des éléments d’observation. La première approche est une modélisation basée sur une spécification de la chaîne d’acquisition. La seconde approche de modélisation est basée sur une implémentation de la chaîne d’acquisition. Les deux modèles sont développés à l’aide des automates temporisés communicants IF. L’évolution et la caractérisation des propriétés temporelles passe par une définition des bases théoriques de l’évaluation du “ retard ” et des règles de l’observation (suivi de la date de production et des dates de consommation).

Le troisième point consiste en l’évaluation du retard proprement dit. L’évaluation et la caractérisation fine des retards d’un pilote d’équipement est réalisée sur plusieurs configurations possibles de la chaine d’acquisition et du pilote d’équipement. Ces configurations sont fonction des paramètres temporels d’une chaine d’acquisition (capteur, pilote, et application de contrôle). L’évaluation du retard est réalisée par l’analyse et la vérification des propriétés sur les STE obtenus après exécution des modèles IF du système. Le retard est présenté sous diverses formes: valeurs (intervalles discrets et continus) de retard possibles en fonction d’un paramètre de la chaîne d’acquisition ou d’un langage du retard (expression régulière) pour une configuration donnée de la chaîne d’acquisition.
to:
%justify% Mes traveaux de recherche propose une approche pour l’évaluation formelle des caractéristiques temporelles des chaines d’acquisition de données dans les systèmes de contrôle de processus. Cette évaluation est basée sur les automates temporisés communicants et les observateurs de propriétés.

%justify% Les résultats obtenus dans ce travail se focalisent sur plusieurs aspects:

%justify% Le premier point consiste
en la mise en place de l’instrumentation d’un observateur d’occurrence pour l’évaluation des propriétés temporelles. L’évaluation des caractéristiques temporelles des occurrences d’un flot de données d’une chaîne d’acquisition nécessite la formalisation du comportement du cycle de vie d’une occurrence de donnée dans une chaîne d’acquisition (production et consommation de l’occurrence, création et suppression de copie, fin de vie de l’occurrence). L’observation des occurrences est orientée pour l’évaluation du “ retard ”.

%justify% Le deuxième point consiste en la modélisation du système, en particulier le pilote d’équipement, et en l’évaluation et la caractérisation fine des propriétés temporelles des retards. La modélisation de la chaine d’acquisition est présentée sous la forme de deux approches de modélisation de la chaîne d’acquisition et des éléments d’observation. La première approche est une modélisation basée sur une spécification de la chaîne d’acquisition. La seconde approche de modélisation est basée sur une implémentation de la chaîne d’acquisition. Les deux modèles sont développés à l’aide des automates temporisés communicants IF. L’évolution et la caractérisation des propriétés temporelles passe par une définition des bases théoriques de l’évaluation du “ retard ” et des règles de l’observation (suivi de la date de production et des dates de consommation).

%justify% Le troisième point consiste en l’évaluation du retard proprement dit. L’évaluation et la caractérisation fine des retards d’un pilote d’équipement est réalisée sur plusieurs configurations possibles de la chaine d’acquisition et du pilote d’équipement. Ces configurations sont fonction des paramètres temporels d’une chaine d’acquisition (capteur, pilote, et application de contrôle). L’évaluation du retard est réalisée par l’analyse et la vérification des propriétés sur les STE obtenus après exécution des modèles IF du système. Le retard est présenté sous diverses formes: valeurs (intervalles discrets et continus) de retard possibles en fonction d’un paramètre de la chaîne d’acquisition ou d’un langage du retard (expression régulière) pour une configuration donnée de la chaîne d’acquisition.
Changed lines 75-78 from:
Une collaboration avec le laboratoire DTN à l’ENSIETA de Brest, sur l’utilisation des α-contextes qui permettent la modélisation de l’environnement de notre pilote d’équipement. Ce travail qui intègre l’utilisation des observateurs de propriété et le temps continu sera prochainement le sujet d’une publication (en cours de rédaction).

L’utilisation du langage de retard fournit par l’approche dans les traveaux de thèse de Julien DeAntoni (l’architecture SAIA). SAIA utilise une description de la QoS en termes de retards, de loi d’arrivée dans le but d’établir un contrat de QoS pour satisfaire qu’un pilote d’équipement particulier satisfait la QoS décrite par la donnée de haut niveau et ainsi assurer la précision du contrôle de l’application. Lors du choix d’un driver spécifique, il leur est alors nécessaire de connaître son langage de QoS, représentant une abstraction temporelle prècise du driver réel. Il réalise alors un simulateur du driver réel en produisant un flot de données conforme à son langage de QoS afin de pouvoir établir le contrat de QoS. Ce travail montre qu’il peut être intéressant de décrire la QoS sous forme d’un langage afin d’avoir une description fine du comportement temporel dans un flot d’acquisition et ainsi de pouvoir en inférer la correction ou non de l’application utilisant ce flot d’acquisition.
to:
%justify% Une collaboration avec le laboratoire DTN à l’ENSIETA de Brest, sur l’utilisation des α-contextes qui permettent la modélisation de l’environnement de notre pilote d’équipement. Ce travail qui intègre l’utilisation des observateurs de propriété et le temps continu sera prochainement le sujet d’une publication (en cours de rédaction).

%justify% L’utilisation du langage de retard fournit par l’approche dans les traveaux de thèse de Julien DeAntoni (l’architecture SAIA). SAIA utilise une description de la QoS en termes de retards, de loi d’arrivée dans le but d’établir un contrat de QoS pour satisfaire qu’un pilote d’équipement particulier satisfait la QoS décrite par la donnée de haut niveau et ainsi assurer la précision du contrôle de l’application. Lors du choix d’un driver spécifique, il leur est alors nécessaire de connaître son langage de QoS, représentant une abstraction temporelle prècise du driver réel. Il réalise alors un simulateur du driver réel en produisant un flot de données conforme à son langage de QoS afin de pouvoir établir le contrat de QoS. Ce travail montre qu’il peut être intéressant de décrire la QoS sous forme d’un langage afin d’avoir une description fine du comportement temporel dans un flot d’acquisition et ainsi de pouvoir en inférer la correction ou non de l’application utilisant ce flot d’acquisition.
Changed lines 80-81 from:
Les travaux menés durant ma thèse sont à la croisée de plusieurs domaines. Aussi, ils m’ont ouverts beaucoup de perspectives de recherche. Dans cette section, je vais aborder trois des points qu’il me parait intéressant d’investiguer.
to:
%justify% Les travaux menés durant ma thèse sont à la croisée de plusieurs domaines. Aussi, ils m’ont ouverts beaucoup de perspectives de recherche. Dans cette section, je vais aborder trois des points qu’il me parait intéressant d’investiguer.
Changed lines 83-86 from:
* L’approche développée permet une caractérisation fine du retard, sous diverses formes (valeurs possibles, langage de retard). Il serait intéressant d’évaluer d’autres caractéristiques temporelles ou non, telles que le taux de perte ou le nombre de pertes successives.
* La mise en place de l’observation (de l’observateur) des occurrences d’un flot de données a été réalisé vis-à-vis du retard malgré le soucis de mettre la notion d’observation d’occurrence en avance. Il serait intéressant de voir par rapport au point précédent les modifications et adaptations de la théorie développée vis-à-vis d’autres caractéristiques. Ceci permettrait de définir une théorie d’observation (observateur) commune par classe ou ensemble des caractéristiques données.
* Certains points dans la théorie de l’observation des occurrences d’un flot de données a été guidé par le formalisme de modélisation utilisée par la suite, à savoir, les automates temporisé et surtout IF. Cependant, d’autres formalismes de modélisation existent (par exemple, les RdPT ), mais aussi d’autres outils (par exemple, UPPAAL, KRONOS ). Il serait intéressant de voir l’influence d’un nouvel outil ou de formalisme de modélisation sur les règles établis durant la mise en place de l’observation d’un flot de données. Ceci permettrait de définir une théorie d’observation (observateur) des occurrences indépendamment du formalisme et de l’outil de modélisation.
to:
* %justify% L’approche développée permet une caractérisation fine du retard, sous diverses formes (valeurs possibles, langage de retard). Il serait intéressant d’évaluer d’autres caractéristiques temporelles ou non, telles que le taux de perte ou le nombre de pertes successives.
* %justify% La mise en place de l’observation (de l’observateur) des occurrences d’un flot de données a été réalisé vis-à-vis du retard malgré le soucis de mettre la notion d’observation d’occurrence en avance. Il serait intéressant de voir par rapport au point précédent les modifications et adaptations de la théorie développée vis-à-vis d’autres caractéristiques. Ceci permettrait de définir une théorie d’observation (observateur) commune par classe ou ensemble des caractéristiques données.
* %justify% Certains points dans la théorie de l’observation des occurrences d’un flot de données a été guidé par le formalisme de modélisation utilisée par la suite, à savoir, les automates temporisé et surtout IF. Cependant, d’autres formalismes de modélisation existent (par exemple, les RdPT ), mais aussi d’autres outils (par exemple, UPPAAL, KRONOS ). Il serait intéressant de voir l’influence d’un nouvel outil ou de formalisme de modélisation sur les règles établis durant la mise en place de l’observation d’un flot de données. Ceci permettrait de définir une théorie d’observation (observateur) des occurrences indépendamment du formalisme et de l’outil de modélisation.
Changed lines 88-90 from:
* Les caractéristiques temporelles, à savoir le retard, évalué dans ce travail concerne la chaîne d’acquisition de données dans les systèmes de contrôle de processus. Cependant, il est important pour les systèmes de contrôle de processus d’évaluer ces mêmes caractéristiques sur la chaîne complète de commandes, à savoir de l’application de contrôle aux actionneurs.
* La mise en place de la théorie de l’observation des occurrences d’un flot de données a été définie indépendamment du type de la donnée manipulée. Il serait intéressant d’adapter et d’appliquer cette théorie dans d’autres systèmes où il y a un flot d’information qui est acheminé entre un élément source et un élément puits. Par analogie, nous pourions nous inspirer de la théorie d’observation développée dans ce travail pour l’évaluation des caractéristiques dans une chaîne de production industrielle, une chaîne de logistique, ou une chaîne de transmission d’information.
to:
* %justify% Les caractéristiques temporelles, à savoir le retard, évalué dans ce travail concerne la chaîne d’acquisition de données dans les systèmes de contrôle de processus. Cependant, il est important pour les systèmes de contrôle de processus d’évaluer ces mêmes caractéristiques sur la chaîne complète de commandes, à savoir de l’application de contrôle aux actionneurs.
* %justify% La mise en place de la théorie de l’observation des occurrences d’un flot de données a été définie indépendamment du type de la donnée manipulée. Il serait intéressant d’adapter et d’appliquer cette théorie dans d’autres systèmes où il y a un flot d’information qui est acheminé entre un élément source et un élément puits. Par analogie, nous pourions nous inspirer de la théorie d’observation développée dans ce travail pour l’évaluation des caractéristiques dans une chaîne de production industrielle, une chaîne de logistique, ou une chaîne de transmission d’information.
Changed line 92 from:
* Dans ce travail de thèse, la modélisation, l’analyse et l’évaluation des caractéristiques temporelles, basés sur l’observation d’un flot de données, sont réalisées par différents outils et formalismes de modélisation, des scripts et des outils d’analyse des STEs. Il serait utile de mettre en place une plateforme intégrée de modélisation et d’analyse des flots de données permettant d’intégrer les divers outils et formalismes de modélisation et d’analyse. Il serait aussi intéressant que la plateforme soit évolutive en acceptant de l’associer à d’autres outils de modélisation ou d’analyse. Dans cette objectif, les outils autour de l’ingéniérie dirigée par les modèles seraient certainement une solution à investiguer.
to:
* %justify% Dans ce travail de thèse, la modélisation, l’analyse et l’évaluation des caractéristiques temporelles, basés sur l’observation d’un flot de données, sont réalisées par différents outils et formalismes de modélisation, des scripts et des outils d’analyse des STEs. Il serait utile de mettre en place une plateforme intégrée de modélisation et d’analyse des flots de données permettant d’intégrer les divers outils et formalismes de modélisation et d’analyse. Il serait aussi intéressant que la plateforme soit évolutive en acceptant de l’associer à d’autres outils de modélisation ou d’analyse. Dans cette objectif, les outils autour de l’ingéniérie dirigée par les modèles seraient certainement une solution à investiguer.
17/12/2008 17:35 by 134.214.106.53 -
Changed line 1 from:
!!!! Thèse
to:
!! Thèse
Changed line 30 from:
!! Systèmes de contrôle/commande, Systèmes temps réel
to:
!!!! Systèmes de contrôle/commande, Systèmes temps réel
Changed line 38 from:
!! Pilote d’équipement
to:
!!!! Pilote d’équipement
Changed line 41 from:
!! Propriétés temporelles des pilotes d’équipement
to:
!!!! Propriétés temporelles des pilotes d’équipement
Changed line 81 from:
!!Extenstions de l’approche
to:
!!!! Extenstions de l’approche
Changed line 86 from:
!! Extentions du domaine d’application
to:
!!!! Extentions du domaine d’application
Changed line 90 from:
!! Mise en œuvre et modèles
to:
!!!! Mise en œuvre et modèles
17/12/2008 17:28 by 134.214.106.53 -
Changed line 14 from:
'''++Jury++''': 
to:
'''[+Jury+]''': 
17/12/2008 17:28 by 134.214.106.53 -
Changed lines 11-12 from:
'''Soutenue le''': 29 Novembre 2008\\
to:
'''Soutenue le''': 29 Novembre 2008
Changed line 14 from:
'''Jury''': 
to:
'''++Jury++''': 
17/12/2008 17:27 by 134.214.106.53 -
Changed lines 9-11 from:
'''Financement''' : EGIDE
'''Date de début''' : 1 mars 2005
'''Soutenue le''': 29 Novembre 2008
to:
'''Financement''' : EGIDE\\
'''Date de début''' : 1 mars 2005\\
'''Soutenue le''': 29 Novembre 2008\\
17/12/2008 17:26 by 134.214.106.53 -
Added lines 5-6:

'''Laboratoire de recherche''' : CITI de l’INSA de Lyon\\
Changed line 8 from:
'''Directeurs de thèse''' : Jean-Philippe Babau (Insa Lyon), Riadh Robbana (EPT Tunisie): Mcfs, habilités à diriger les recherches
to:
'''Directeurs de thèse''' : Pr. Jean-Philippe Babau (UBO Brest), Pr. Riadh Robbana (EPT Tunisie)
Changed lines 13-26 from:
Titre:
to:
'''Jury''':  
     
'''Président''' 
-> Belhassen Zouari - Professeur à la Faculté des Sciences de Bizerte, Tunisie
'''Rapporteurs''' 
-> Néjib Ben Hadj-Alouane - Professeur à L’ENSI - Tunisie
-> Frédéric Boniol - Professeur à ENSEEIHT de Toulouse
'''Examinateurs'''
-> Philippe Dhaussy - Enseignant-Chercheur à ENSIETA Brest
-> Fabrice Jumel - Enseignant-Chercheur à ESCPE Lyon (Co-encadrant de thèse)
-> Jean Philippe Babau - Professeur à l’UBO Brest (Directeur de thèse)
-> Riadh Robbana - Professeur à l’EPT, Tunisie (Co-directeur de thèse)

 
Changed lines 28-43 from:
Evaluation des propriétés des pilotes d’équipement
to:
!!! Contexte
!! Systèmes de contrôle/commande, Systèmes temps réel
Les systèmes de contrôle de processus, c’est-à-dire les systèmes en charge du suivi et/ou du contrôle d’un processus physique auquel ils sont liés, sont présents dans des nombreux secteurs d’activités (système de contrôle de production, ferroviaire, avionique, spatiale ou encore domotique). Ces systèmes informatiques dont le comportement dépend de l’évolution du processus qu’ils contrôlent sont critiques: une défaillance du contrôle peut avoir des conséquences catastrophiques.

Les systèmes de contrôle de processus sont des systèmes réactifs qui contrôlent en temps réel leur environnement physique. Du fait de l’évolution dynamique du processus, les systèmes de contrôle commandent le processus en fonction des “ informations ” ou des données mesurées sur ce dernier et traduisant son évolution, dans un temps contraint pour assurer un contrôle correct.
Les spécificités temps réel des systèmes de contrôle de processus influent le processus de développement. En particulier, une évaluation des caractéristiques temporelles lors du développement est nécessaire pour assurer leur validation. Ainsi, si les caractéristiques (les lois) temporelles des flots d’informations en provenance ou à destination de processus ne sont pas prises en compte lors de développement, la validation du système est incorrecte vis-à-vis des propriétés temporelles qu’il doit satisfaire.

En effet, le système de contrôle évolue, non seulement en fonction des valeurs des informations “ en entrée ”, mais aussi en fonction de leur qualité d’acquisition (précision, retard,...).

!! Pilote d’équipement
Ce flot d’informations en “entrée” d’un système de contrôle de processus est construit par un ensemble de composants de mesure appelés “ capteurs ”, et à destination de l’application de contrôle. De plus, les systèmes de contrôle de processus intègrent un (ou plusieurs) composant logiciel appelé “ pilote d’équipement ” permettant de fournir une interface entre l’application et l’équipement (ici le ou les capteurs). Le pilote d’équipement est un composant logiciel qui affecte d’une manière importante la qualité des informations transmises à l’application de contrôle et donc la qualité des systèmes. Le pilote de capteur ou pilote d’acquisition est un composant critique du système, il est à l’origine de plusieurs bugs et crashs des systèmes de contrôle de processus.

!! Propriétés temporelles des pilotes d’équipement
La validation des propriétés temporelles des systèmes de contrôle de processus se base sur une connaissance des caractéristiques temporelles des flots d’informations en “ entrée ” du système de contrôle. La caractérisation de flots d’information acheminés à partir des capteurs à l’application de contrôle se traduit par une évaluation des caractéristiques temporelles de cette la chaîne d’acquisition. Vu le contexte temps réel des systèmes de contrôle de processus cette validation se doit d’être exhaustive et formelle.

!!! Évaluation
des propriétés des pilotes d’équipement
Added lines 45-52:

La validation des propriétés temporelles des pilotes des systèmes d’acquisition pour le contrôle de processus s’effectue alors en plusieurs étapes:
* Identifier les propriétés temporelles à vérifier pour le système d’aquisition vis-à-vis du système de contrôle.
* Modéliser le système et son pilote d’équipement.
* Choisir un langage (et outils associés) pour la formalisation des modèles.
* Analyser et vérifier des propriétés.
* Paramétrer le pilote d’équipement et le système de contrôle en fonction des résultats trouvé lors des étapes précédentes.

Changed lines 54-57 from:
 Définir mathématiquement les propriétés des QoS à vérifier à l’aide de logique temps réel (RTL).
L’utilisation des automates observateurs pour récupérer les mesures souhaitées afin de résoudre les problèmes de l’explosion combinatoire que l’on a rencontré.
Le développement d’un pilote d’équipement sous linux temps réel (RTAI) (travail effectué dans le cadre d’un projet de fin d’étude DUT), puis sous VxWorks afin d’avoir des résultats réels pour les comparer avec les résultats trouvés avec IF (les premiers résultats sont très proches de ceux calculés avec IF). Ce travail a permis aussi d’avoir des traces de mesures de performance qu’on utilisera afin de donner une caractérisation stochastique de notre modèle.
L’utilisation de temps continu pour la simulation IF à la place de temps discret utilisé jusqu’à présent.
to:
* Définir mathématiquement les propriétés des QoS à vérifier à l’aide de logique temps réel (RTL).
* L’utilisation des automates observateurs pour récupérer les mesures souhaitées afin de résoudre les problèmes de l’explosion combinatoire que l’on a rencontré.
* Le développement d’un pilote d’équipement sous linux temps réel (RTAI) (travail effectué dans le cadre d’un projet de fin d’étude DUT), puis sous VxWorks afin d’avoir des résultats réels pour les comparer avec les résultats trouvés avec IF (les premiers résultats sont très proches de ceux calculés avec IF). Ce travail a permis aussi d’avoir des traces de mesures de performance qu’on utilisera afin de donner une caractérisation stochastique de notre modèle.
* L’utilisation de temps continu pour la simulation IF à la place de temps discret utilisé jusqu’à présent.
Changed lines 60-63 from:
 L’ensemble de ces travaux ont conduit aux résultats suivants:
 La formalisation de mon approche et surtout la formalisation des observateurs de propriétés. Ce travail était réalisé en collaboration avec le directeur tunisien de la thèse, il sera prochainement le sujet d’une publication.
Une collaboration avec le laboratoire DTN à l’ENSIETA de Brest, sur l’utilisation des α-contextes qui permettent la modélisation de l’environnement de notre pilote d’équipement. Ce travail qui intègre l’utilisation des observateurs de propriété et le temps continu sera prochainement le sujet d’une publication (en cours de rédaction).
Ces resultats ont fait l’objet de deux publications [3] [4] et un rapport de recherche [6].
to:
 
!!! Contributions
Mes traveaux de recherche propose une approche pour l’évaluation formelle des caractéristiques temporelles des chaines d’acquisition de données dans les systèmes de contrôle de processus. Cette évaluation est basée sur les automates temporisés communicants et les observateurs de propriétés.

Les résultats obtenus dans ce travail se focalisent sur plusieurs aspects.
Le premier point consiste en la mise en place de l’instrumentation d’un observateur d’occurrence pour l’évaluation des propriétés temporelles. L’évaluation des caractéristiques temporelles des occurrences d’un flot de données d’une chaîne d’acquisition nécessite la formalisation du comportement du cycle de vie d’une occurrence de donnée dans une chaîne d’acquisition (production et consommation de l’occurrence, création et suppression de copie, fin de vie de l’occurrence). L’observation des occurrences est orientée pour l’évaluation du “ retard ”.

Le deuxième point consiste en la modélisation du système, en particulier le pilote d’équipement, et en l’évaluation et la caractérisation fine des propriétés temporelles des retards. La modélisation de la chaine d’acquisition est présentée sous la forme de deux approches de modélisation de la chaîne d’acquisition et des éléments d’observation. La première approche est une modélisation basée sur une spécification de la chaîne d’acquisition. La seconde approche de modélisation est basée sur une implémentation de la chaîne d’acquisition. Les deux modèles sont développés à l’aide des automates temporisés communicants IF. L’évolution et la caractérisation des propriétés temporelles passe par une définition des bases théoriques de l’évaluation du “ retard ” et des règles de l’observation (suivi de la date de production et des dates de consommation).

Le troisième point consiste en l’évaluation du retard proprement dit. L’évaluation et la caractérisation fine des retards d’un pilote d’équipement est réalisée sur plusieurs configurations possibles de la chaine d’acquisition et du pilote d’équipement. Ces configurations sont fonction des paramètres temporels d’une chaine d’acquisition (capteur, pilote, et application de contrôle). L’évaluation du retard est réalisée par l’analyse et la vérification des propriétés sur les STE obtenus après exécution des modèles IF du système. Le retard est présenté sous diverses formes: valeurs (intervalles discrets et continus) de retard possibles en fonction d’un paramètre de la chaîne d’acquisition ou d’un langage du retard (expression régulière) pour une configuration donnée de la chaîne d’acquisition.

Ces resultats ont fait l’objet de deux publications [3] [4] et un rapport de recherche [6].

Une collaboration avec le laboratoire DTN à l’ENSIETA de Brest, sur l’utilisation des α-contextes qui permettent la modélisation de l’environnement de notre pilote d’équipement. Ce travail qui intègre l’utilisation des observateurs de propriété et le temps continu sera prochainement le sujet d’une publication (en cours de rédaction).

L’utilisation du langage de retard fournit par l’approche dans les traveaux de thèse de Julien DeAntoni (l’architecture SAIA). SAIA utilise une description de la QoS en termes de retards, de loi d’arrivée dans le but d’établir un contrat de QoS pour satisfaire qu’un pilote d’équipement particulier satisfait la QoS décrite par la donnée de haut niveau et ainsi assurer la précision du contrôle de l’application. Lors du choix d’un driver spécifique, il leur est alors nécessaire de connaître son langage de QoS, représentant une abstraction temporelle prècise du driver réel. Il réalise alors un simulateur du driver réel en produisant un flot de données conforme à son langage de QoS afin de pouvoir établir le contrat de QoS. Ce travail montre qu’il peut être intéressant de décrire la QoS sous forme d’un langage afin d’avoir une description fine du comportement temporel dans un flot d’acquisition et ainsi de pouvoir en inférer la correction ou non de l’application utilisant ce flot d’acquisition.

!!! Perspectives scientifiques
Les travaux menés durant ma thèse sont à la croisée de plusieurs domaines. Aussi, ils m’ont ouverts beaucoup de perspectives de recherche. Dans cette section, je vais aborder trois des points qu’il me parait intéressant d’investiguer.

!!Extenstions de l’approche
* L’approche développée permet une caractérisation fine du retard, sous diverses formes (valeurs possibles, langage de retard). Il serait intéressant d’évaluer d’autres caractéristiques temporelles ou non, telles que le taux de perte ou le nombre de pertes successives.
* La mise en place de l’observation (de l’observateur) des occurrences d’un flot de données a été réalisé vis-à-vis du retard malgré le soucis de mettre la notion d’observation d’occurrence en avance. Il serait intéressant de voir par rapport au point précédent les modifications et adaptations de la théorie développée vis-à-vis d’autres caractéristiques. Ceci permettrait de définir une théorie d’observation (observateur) commune par classe ou ensemble des caractéristiques données.
* Certains points dans la théorie de l’observation des occurrences d’un flot de données a été guidé par le formalisme de modélisation utilisée par la suite, à savoir, les automates temporisé et surtout IF. Cependant, d’autres formalismes de modélisation existent (par exemple, les RdPT ), mais aussi d’autres outils (par exemple, UPPAAL, KRONOS ). Il serait intéressant de voir l’influence d’un nouvel outil ou de formalisme de modélisation sur les règles établis durant la mise en place de l’observation d’un flot de données. Ceci permettrait de définir une théorie d’observation (observateur) des occurrences indépendamment du formalisme et de l’outil de modélisation.

!! Extentions du domaine d’application
* Les caractéristiques temporelles, à savoir le retard, évalué dans ce travail concerne la chaîne d’acquisition de données dans les systèmes de contrôle de processus. Cependant, il est important pour les systèmes de contrôle de processus d’évaluer ces mêmes caractéristiques sur la chaîne complète de commandes, à savoir de l’application de contrôle aux actionneurs.
* La mise en place de la théorie de l’observation des occurrences d’un flot de données a été définie indépendamment du type de la donnée manipulée. Il serait intéressant d’adapter et d’appliquer cette théorie dans d’autres systèmes où il y a un flot d’information qui est acheminé entre un élément source et un élément puits. Par analogie, nous pourions nous inspirer de la théorie d’observation développée dans ce travail pour l’évaluation des caractéristiques dans une chaîne de production industrielle, une chaîne de logistique, ou une chaîne de transmission d’information.

!! Mise en œuvre et modèles
* Dans ce travail de thèse, la modélisation, l’analyse et l’évaluation des caractéristiques temporelles, basés sur l’observation d’un flot de données, sont réalisées par différents outils et formalismes de modélisation, des scripts et des outils d’analyse des STEs. Il serait utile de mettre en place une plateforme intégrée de modélisation et d’analyse des flots de données permettant d’intégrer les divers outils et formalismes de modélisation et d’analyse. Il serait aussi intéressant que la plateforme soit évolutive en acceptant de l’associer à d’autres outils de modélisation ou d’analyse. Dans cette objectif, les outils autour de l’ingéniérie dirigée par les modèles seraient certainement une solution à investiguer.
05/12/2008 16:38 by 82.229.16.111 -
Changed line 9 from:
'''Soutenue le: 29 Novembre 2008
to:
'''Soutenue le''': 29 Novembre 2008
05/12/2008 16:37 by 82.229.16.111 -
Changed lines 3-44 from:
%color=blue define=Analyse% '''Analyse de la qualité de service des systèmes temps réel d’acquisition de  données : Une approche à base d’automates communicants temporisés.'''

'''Encadrement scientifique:''' Fabrice Jumel (mailto:fabrice.jumel@insa-lyon.fr) [[http://citi.insa-lyon.fr|CITI]], [[http://www.bbhedia.org/robbana|Riadh ROBBANA]] (mailto:riadh.robbana@fst.rnu.tn) LIP2 

'''Responsable au sein des laboratoires:''' [[http
://www.lisyc.univ-brest.fr/pages_perso/babau|Jean Philippe BABAU]] (responsable de l’équipe temps réel du [[http://citi.insa-lyon.fr|CITI]]), Stéphane Ubéda (directeur du [[http://citi.insa-lyon.fr|CITI]]). Mohamed Moalla (directeur de LIP2).

* '''Contexte'''
Le travail s’inscrit dans le cadre des systèmes réactifs temps réel sujet à des contraintes temporelles fortes. Cette classe de systèmes est présente dans plusieurs domaines, en particulier dans la conduite de procédés industriels et la robotique
.
Les systèmes réactifs temps réel sont des systèmes qui doivent réagir aux stimuli en provenance du procédé à contrôler dans un délai fixe donné. Du fait de la multiplicité des stimuli et de la diversité des contraintes, ces systèmes sont des systèmes concurrents. Classiquement l’implémentation de tels systèmes aboutit à une application multitâche dont les actions sont décrites dans un langage de haut niveau de type C. La gestion de la concurrence s’appuie sur les services offerts par un système d’exploitation temps réel (RTOS).
Les domaines d’application souvent critiques
des systèmes réactifs temps réel exigent une validation temporelle du système a priori. Cette validation s’appuie sur des modèles formels orientés QoS (Qualité de Service) pour caractériser les systèmes considérés ainsi que les propriétés de QoS attendues. La validation consiste alors à vérifier que les propriétés de QoS du système sont correctes en regard des propriétés de QoS attendues.

* '''Projet'''
Les techniques classiques d’analyse de la QoS et les langages de modélisation
de la QoS s’appuie généralement sur des modèles statiques (analyse RMA [1], modèles UML du profil SPT [2] , architecture distribuée pour le temps réel [3]). Une première étude [4] a montré les limites des descriptions statiques dans le cadre des systèmes d’acquisition des données. De plus, des travaux récents ont démontré l’apport de techniques d’analyse basées sur les automates temporisés pour intégrer  des aspects dynamiques dans le comportement des systèmes étudiés [5, 6]. Toutes ces études apportent du réalisme dans l’analyse des propriétés temporelles des systèmes, réalisme indispensable à la validation des systèmes [7].
Dans ce cadre, le travail proposé concerne la modélisation formelle à base d’automates temporisés ( tels que IF [8] ou UPPAAL [10] IF est une représentation intermédiaire entre les Timed automata et SDL, UPPAAL est un Model-checker qui utilise comme modèles d’entrées les automates temporisés on peut aussi rajouter Kronos, je pense qu’il vaut mieux enlever toute cette parenthèse et mettre quelques références relatives aux automates temporisés) d’une implémentation multitâche pour un système de contrôle
de procédé. A partir des modèles proposés, des techniques seront développées (telles que la bi-simulation [9] : la bi-simulation ne permet pas d’extraire des propriétés, elle permet comme son nom l’indique de voir si deux modèles sont bi-similaires, je propose plutôt la synthèse d'invariants dans ce cadre il serait intéressant de voir les travaux de Y.Lakhnech et S.Bensalem du coté de VERIMAG et de N.Shankar, A.Tiwari, H. Ruess et H. Saidi du coté du SRI que nous pouvons entre autres trouver dans TACAS"01) pour extraire des propriétés de QoS appelées, dans ce contexte, qualité de fonctionnement ou QdF. Par QdF, on entend des propriétés de performance telles que le temps de réponse ou retard, la gigue, la précision, le taux de fautes, etc. Cette étude concerne le domaine des applications de robotique. Les propriétés de QdF considérées ainsi que les implémentations sont donc celles liées aux spécificités du domaine.
Au final, les travaux de thèse ont pour objectifs, dans un premier temps, de proposer (un langage semi-formel dédié à la programmation du procédé, de l'interface de communication, de l'application et de l'architecture matérielle puis de faire une translation de ce langage ou d'une partie de celui-ci vers les automates temporisés pour des fins de vérification pour cela on pourra peut être utiliser le modèle de représentation intermédiaire IF. Le doctorant pourra par la suite voir s'il peut extraire des propriétés de QdF à partir de son programme initial ou bien à partir de l'automate temporisé associé voire même des deux...) des modèles formels prenant en considération le procédé (robot), l’interface de communication, l’application et l’architecture matérielle. A partir de ces modèles l’étude donnera les moyens d’obtention des propriétés de QdF du système modélisé.
Dans un second temps, nous proposons d’étudier l’impact du choix d’une architecture d’implémentation sur les propriétés de QdF obtenues. Le but étant de proposer des méthodologies de choix ou d’adaptation d’architecture d’implémentation.

* '''Références'''
** [1] M. Klein & all “A practionner’s Handbook for Real-Time Analysis ”, Kluwer Academic Publishers, 1993.
** [2] OMG “ UML Profile for Schedulability, Performance and Time Specification ”, Mar 2002. http://www.omg.org/cgi-bin/doc?ptc/02-03-02.pdf.
** [3] S. Neema, T. Bapty, J. Gray, and A. Gokhale “ Generators for Synthesis of QoS Adaptation in Distributed Real-Time Embedded Systems ”, GPCE 2002, Springer-Verlag, LNCS 2487, pp. 236–251
** [4] B. Ben Hedia « Modélisation formelle d’un driver d’acquisition des données » rapport de stage de DEA, Juillet 2004.
** [5] M. Berlarbi « Validation temporelle des applications multitâches temps réel basée sur les automates communicants » thèse de doctorat, CITI - Insa de Lyon,  décembre 2003.
** [6] K. Altisen, G. Goessler, J. Sifakis “ Scheduler Modeling Based on the Controller Synthesis Paradigm ”, Real-Time Systems Journal, Vol 23(1/2), pp 55-84, Kluwer, 2002.
** [7] F. Jumel « Définition et gestion d’une qualité de service pour les applications temps réel » thèse de doctorat, INPL Nancy, septembre 2003.
** [8] M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier “ IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems ”, FM'99, Toulouse, 1999.
** [9] J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, M. Sighireanu “ CADP A Protocol Validation and Verification Toolbox ”, 8th International Conference on Computer Aided Verification CAV, New Brunswick (USA),1996.
** [10] UPPAAL http://www.uppaal.com/


!!!! DEA et PFE
----

* '''Résumé de DEA'''
Le travail de mon DEA s’inscrit dans le cadre des systèmes réactifs temps réel. Sujet à des contraintes temporelles fortes, cette classe de systèmes est présente dans plusieurs domaines tels que la conduite de procédés industriels, la robotique, l’aéronautique, les systèmes de téléopération et les télécommunications.
Les domaines d’application des systèmes réactifs temps réel critiques exigent une validation formelle du système, appelé validation temps réel. Cette validation s’appuie sur des modèles formels des propriétés de QoS (qualité de service).
Le travail présenté concerne la modélisation formelle et l’analyse des qualités de service pour un système d’acquisition des données. Dans un premier temps, nous proposons des modèles formels tout en prenant en considération le procédé, l’interface de communication ainsi que l’application. Ces différentes composantes constituent notre système d’acquisition des données. Les modèles proposés sont basés sur le langage formel IF. Dans un second temps, nous étudions les propriétés de qualité de service (QoS) ainsi que leurs impacts sur le choix d’une architecture pour un système d’acquisition des données.

'''Mots-Clés''' : ''temps-réel, acquisition des données, pilote, validation formelle, système de contrôle commande, qualité de service.''

* '''Résumé de PFE'''
La modélisation et le choix d’une architecture matérielle pour un système embarqué fait l'objet de nombreuses recherches approfondies au sein de plusieurs laboratoires dans le monde. Certes, plusieurs solutions existantes permettent la modélisation et le choix de l’architecture mais souvent, les outils de modélisation impose des diagrammes de représentation restrictives et intégrant logiciel et matériel dans le même diagramme. L'objectif de mon stage est de mettre en œuvre à l’aide des diagramme d’UML un modèle générique d’architecture matérielle. Ce modèle doit permettre de représenter toute architecture matérielle spécifique dans le même formalisme UML. Ce travail est appliqué au cas de l’architecture du Robot Pioneer2, et constitue un premier pas vers le développement des patterns de conception d’une architecture matérielle
.
to:
%color=blue define=Analyse% '''Analyse temporelle des systèmes d’acquisition de données : une approche à base d’automates temporisés communicants et d’observateurs.'''

'''Équipe d’accueil''' : Axe systèmes embarqués\\
'''Directeurs de thèse'''
: Jean-Philippe Babau (Insa Lyon), Riadh Robbana (EPT Tunisie): Mcfs, habilités à diriger les recherches
'''Financement'''
: EGIDE
'''Date de début''' : 1 mars 2005
'''Soutenue le: 29 Novembre 2008
 
Titre
:
Dans le cadre de mes activités de recherche, je m’intéresse à la validation temporelle des applications temps réel. Dans mes travaux de thèse, nous avons défini une méthodologie d’évaluation des propriétés temporelles (par exemple les délais d’acheminement d’une donnée) des pilotes d’équipement des applications temps réel embarquées
. Enfin, j’ai eu l’occasion, au cours de mes recherches, de m’intéresser aux environnements de spécification, conception, modélisation et validation des applications temps réel tels que l’outil IF, les automates temporisés communicants, la boîte à outil CADP.
Evaluation
des propriétés des pilotes d’équipement
J’ai débuté mon travail de recherche par un travail de modélisation des systèmes d’acquisition des données. J’ai étudié la sémantique des automates temporisés communicants dans IF, l’instrumentation de modèle pour extraire les propriétés temporelles cherchées. Ceci m’a permis de donner dans MSR 05 [1] et FDL 05 [2]
des résultats d’évaluation des propriétés temporelles (par exemple le retard) sur des exemples complexes et réalistes et une comparaison avec des résultats obtenus avec une méthode analytique basée sur l’ordonnancement. Ceci a permis de montrer l’intérêt d’une modélisation à l’aide des automates temporisés et l’analyse exhaustive des modèles. Les résultats obtenus présentes des détails qu’on ne trouve pas à l’aide d’une approche analytique qui ne donne que des bornes. La possibilité de prendre en compte une modélisation des temps de traitements variables (liés à une analyse d’ordonnancement) et ainsi de faire le lien entre les pilotes d’équipements, la politique d’ordonnancement et le choix des paramètres (priorité des tâches), nous a permis d’étudier des exemples beaucoup plus réalistes et beaucoup plus complexes.
Nous avons commencé par la suite plusieurs travaux afin de résoudre quelques problèmes :
 Définir mathématiquement les propriétés des QoS à vérifier à l’aide de logique temps réel (RTL).
L’utilisation des automates observateurs pour récupérer les mesures souhaitées afin de résoudre les problèmes de l’explosion combinatoire que l’on a rencontré.
Le développement d’un pilote d’équipement sous linux temps réel (RTAI) (travail effectué dans le cadre d’un projet de fin d’étude DUT), puis sous VxWorks afin d’avoir des résultats réels pour les comparer avec les résultats trouvés avec IF (les premiers résultats sont très proches de ceux calculés avec IF). Ce travail a permis aussi d’avoir des traces de mesures de performance qu’on utilisera afin de donner une caractérisation stochastique de notre modèle.
L’utilisation
de temps continu pour la simulation IF à la place de temps discret utilisé jusqu’à présent.
Depuis le début de la thèse l’approche utilisée était de proposer un modèle de système d’acquisition (spécialement de pilote d’équipement) puis d’instrumenter ce modèle afin d’évaluer les propriétés de QoS. Après avoir développé un pilote d’équipement et afin d’avoir des modèles plus réalistes, j’ai modifié mon approche, la nouvelle approche propose un modèle de pilote d’équipement basé sur les architectures logiciels des implémentations des pilotes d’équipement (implémentation réalisée sous VxWorks). Cette approche m’a permis d’avoir un modèle plus réaliste, l’observation de ce modèle à l’aide des observateurs (un observateur pour chaque propriété à évaluer) a permis d’avoir une évaluation de la QoS en fonction des paramètres du pilote d’équipement.
 L’ensemble de ces travaux ont conduit aux résultats suivants:
 La formalisation de mon approche et surtout la formalisation des observateurs de propriétés
. Ce travail était réalisé en collaboration avec le directeur tunisien de la thèse, il sera prochainement le sujet d’une publication.
Une collaboration avec le laboratoire DTN à l’ENSIETA
de Brest, sur l’utilisation des α-contextes qui permettent la modélisation de l’environnement de notre pilote d’équipement. Ce travail qui intègre l’utilisation des observateurs de propriété et le temps continu sera prochainement le sujet d’une publication (en cours de rédaction).
Ces resultats ont fait l’objet de deux publications [3] [4] et un rapport
de recherche [6].
30/11/2008 20:14 by 82.235.44.69 -
Added lines 1-44:
!!!! Thèse
----
%color=blue define=Analyse% '''Analyse de la qualité de service des systèmes temps réel d’acquisition de  données : Une approche à base d’automates communicants temporisés.'''

'''Encadrement scientifique:''' Fabrice Jumel (mailto:fabrice.jumel@insa-lyon.fr) [[http://citi.insa-lyon.fr|CITI]], [[http://www.bbhedia.org/robbana|Riadh ROBBANA]] (mailto:riadh.robbana@fst.rnu.tn) LIP2 

'''Responsable au sein des laboratoires:''' [[http://www.lisyc.univ-brest.fr/pages_perso/babau|Jean Philippe BABAU]] (responsable de l’équipe temps réel du [[http://citi.insa-lyon.fr|CITI]]), Stéphane Ubéda (directeur du [[http://citi.insa-lyon.fr|CITI]]). Mohamed Moalla (directeur de LIP2).

* '''Contexte'''
Le travail s’inscrit dans le cadre des systèmes réactifs temps réel sujet à des contraintes temporelles fortes. Cette classe de systèmes est présente dans plusieurs domaines, en particulier dans la conduite de procédés industriels et la robotique.
Les systèmes réactifs temps réel sont des systèmes qui doivent réagir aux stimuli en provenance du procédé à contrôler dans un délai fixe donné. Du fait de la multiplicité des stimuli et de la diversité des contraintes, ces systèmes sont des systèmes concurrents. Classiquement l’implémentation de tels systèmes aboutit à une application multitâche dont les actions sont décrites dans un langage de haut niveau de type C. La gestion de la concurrence s’appuie sur les services offerts par un système d’exploitation temps réel (RTOS).
Les domaines d’application souvent critiques des systèmes réactifs temps réel exigent une validation temporelle du système a priori. Cette validation s’appuie sur des modèles formels orientés QoS (Qualité de Service) pour caractériser les systèmes considérés ainsi que les propriétés de QoS attendues. La validation consiste alors à vérifier que les propriétés de QoS du système sont correctes en regard des propriétés de QoS attendues.

* '''Projet'''
Les techniques classiques d’analyse de la QoS et les langages de modélisation de la QoS s’appuie généralement sur des modèles statiques (analyse RMA [1], modèles UML du profil SPT [2] , architecture distribuée pour le temps réel [3]). Une première étude [4] a montré les limites des descriptions statiques dans le cadre des systèmes d’acquisition des données. De plus, des travaux récents ont démontré l’apport de techniques d’analyse basées sur les automates temporisés pour intégrer  des aspects dynamiques dans le comportement des systèmes étudiés [5, 6]. Toutes ces études apportent du réalisme dans l’analyse des propriétés temporelles des systèmes, réalisme indispensable à la validation des systèmes [7].
Dans ce cadre, le travail proposé concerne la modélisation formelle à base d’automates temporisés ( tels que IF [8] ou UPPAAL [10] IF est une représentation intermédiaire entre les Timed automata et SDL, UPPAAL est un Model-checker qui utilise comme modèles d’entrées les automates temporisés on peut aussi rajouter Kronos, je pense qu’il vaut mieux enlever toute cette parenthèse et mettre quelques références relatives aux automates temporisés) d’une implémentation multitâche pour un système de contrôle de procédé. A partir des modèles proposés, des techniques seront développées (telles que la bi-simulation [9] : la bi-simulation ne permet pas d’extraire des propriétés, elle permet comme son nom l’indique de voir si deux modèles sont bi-similaires, je propose plutôt la synthèse d'invariants dans ce cadre il serait intéressant de voir les travaux de Y.Lakhnech et S.Bensalem du coté de VERIMAG et de N.Shankar, A.Tiwari, H. Ruess et H. Saidi du coté du SRI que nous pouvons entre autres trouver dans TACAS"01) pour extraire des propriétés de QoS appelées, dans ce contexte, qualité de fonctionnement ou QdF. Par QdF, on entend des propriétés de performance telles que le temps de réponse ou retard, la gigue, la précision, le taux de fautes, etc. Cette étude concerne le domaine des applications de robotique. Les propriétés de QdF considérées ainsi que les implémentations sont donc celles liées aux spécificités du domaine.
Au final, les travaux de thèse ont pour objectifs, dans un premier temps, de proposer (un langage semi-formel dédié à la programmation du procédé, de l'interface de communication, de l'application et de l'architecture matérielle puis de faire une translation de ce langage ou d'une partie de celui-ci vers les automates temporisés pour des fins de vérification pour cela on pourra peut être utiliser le modèle de représentation intermédiaire IF. Le doctorant pourra par la suite voir s'il peut extraire des propriétés de QdF à partir de son programme initial ou bien à partir de l'automate temporisé associé voire même des deux...) des modèles formels prenant en considération le procédé (robot), l’interface de communication, l’application et l’architecture matérielle. A partir de ces modèles l’étude donnera les moyens d’obtention des propriétés de QdF du système modélisé.
Dans un second temps, nous proposons d’étudier l’impact du choix d’une architecture d’implémentation sur les propriétés de QdF obtenues. Le but étant de proposer des méthodologies de choix ou d’adaptation d’architecture d’implémentation.

* '''Références'''
** [1] M. Klein & all “A practionner’s Handbook for Real-Time Analysis ”, Kluwer Academic Publishers, 1993.
** [2] OMG “ UML Profile for Schedulability, Performance and Time Specification ”, Mar 2002. http://www.omg.org/cgi-bin/doc?ptc/02-03-02.pdf.
** [3] S. Neema, T. Bapty, J. Gray, and A. Gokhale “ Generators for Synthesis of QoS Adaptation in Distributed Real-Time Embedded Systems ”, GPCE 2002, Springer-Verlag, LNCS 2487, pp. 236–251
** [4] B. Ben Hedia « Modélisation formelle d’un driver d’acquisition des données » rapport de stage de DEA, Juillet 2004.
** [5] M. Berlarbi « Validation temporelle des applications multitâches temps réel basée sur les automates communicants » thèse de doctorat, CITI - Insa de Lyon,  décembre 2003.
** [6] K. Altisen, G. Goessler, J. Sifakis “ Scheduler Modeling Based on the Controller Synthesis Paradigm ”, Real-Time Systems Journal, Vol 23(1/2), pp 55-84, Kluwer, 2002.
** [7] F. Jumel « Définition et gestion d’une qualité de service pour les applications temps réel » thèse de doctorat, INPL Nancy, septembre 2003.
** [8] M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier “ IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems ”, FM'99, Toulouse, 1999.
** [9] J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, M. Sighireanu “ CADP A Protocol Validation and Verification Toolbox ”, 8th International Conference on Computer Aided Verification CAV, New Brunswick (USA),1996.
** [10] UPPAAL http://www.uppaal.com/


!!!! DEA et PFE
----

* '''Résumé de DEA'''
Le travail de mon DEA s’inscrit dans le cadre des systèmes réactifs temps réel. Sujet à des contraintes temporelles fortes, cette classe de systèmes est présente dans plusieurs domaines tels que la conduite de procédés industriels, la robotique, l’aéronautique, les systèmes de téléopération et les télécommunications.
Les domaines d’application des systèmes réactifs temps réel critiques exigent une validation formelle du système, appelé validation temps réel. Cette validation s’appuie sur des modèles formels des propriétés de QoS (qualité de service).
Le travail présenté concerne la modélisation formelle et l’analyse des qualités de service pour un système d’acquisition des données. Dans un premier temps, nous proposons des modèles formels tout en prenant en considération le procédé, l’interface de communication ainsi que l’application. Ces différentes composantes constituent notre système d’acquisition des données. Les modèles proposés sont basés sur le langage formel IF. Dans un second temps, nous étudions les propriétés de qualité de service (QoS) ainsi que leurs impacts sur le choix d’une architecture pour un système d’acquisition des données.

'''Mots-Clés''' : ''temps-réel, acquisition des données, pilote, validation formelle, système de contrôle commande, qualité de service.''

* '''Résumé de PFE'''
La modélisation et le choix d’une architecture matérielle pour un système embarqué fait l'objet de nombreuses recherches approfondies au sein de plusieurs laboratoires dans le monde. Certes, plusieurs solutions existantes permettent la modélisation et le choix de l’architecture mais souvent, les outils de modélisation impose des diagrammes de représentation restrictives et intégrant logiciel et matériel dans le même diagramme. L'objectif de mon stage est de mettre en œuvre à l’aide des diagramme d’UML un modèle générique d’architecture matérielle. Ce modèle doit permettre de représenter toute architecture matérielle spécifique dans le même formalisme UML. Ce travail est appliqué au cas de l’architecture du Robot Pioneer2, et constitue un premier pas vers le développement des patterns de conception d’une architecture matérielle.