Thèse


Analyse temporelle des systèmes d’acquisition de données : une approche à base d’automates temporisés communicants et d’observateurs.

Manuscrit: (ici )
Présentation: (ici )

Laboratoire de recherche : CITI de l’INSA de Lyon
Équipe d’accueil : Axe systèmes embarqués
Directeurs de thèse : Pr. Jean-Philippe Babau (UBO Brest), Pr. Riadh Robbana (EPT Tunisie) Financement : EGIDE
Date de début : 1 mars 2005
Soutenue le: 29 Novembre 2008

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)

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.

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

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.

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.