IRIT - UMR 5505

Historiquement, l’intérêt de l’équipe Acadie porte sur :

• la construction de la preuve formelle d’algorithmes distribués :prouver formellement un algorithme existant, afin de mettre en évidence des structures (de donnée ou de code) communes à une classe d’algorithmes et de faire émerger des schémas de preuve réutilisables ;
• le développement formel d’algorithmes distribués : partir de la spécification formelle d’un problème et le raffiner pour obtenir un algorithme implantable et garanti correct. Tout naturellement, l’équipe a intégré les aspects temps-réel et embarqués pour ses travaux effectués au cours de 2005-2008.

Algorithmique distribuée

La collaboration avec l’équipe Vortex a été poursuivie en étudiant des algorithmes de diffusions dans un cadre multimédia réellement réparti (plusieurs sources, plusieurs destinataires, plusieurs flux : applications Computer Supported Cooperative Work). Nous avons montré comment coordonner des flux répartis (thèse Cezar Plesca 04-07 [9043]).

Systèmes satellitaires et DRE

Les DRE (Distributed Real-time Embedded systems), fusion de l’algorithmique distribuée, des systèmes temps-réel et des systèmes embarqués, nécessitent des techniques de preuve à cheval sur ces domaines. Nous avons étudié la description d’un système temps-réel réparti exclusivement par les données et leurs circulations, sans avoir à considérer la décomposition en tâches et leur ordonnancement. Les interactions entre données sont abstraites via une relation qui lie les valeurs de deux variables en y attachant des contraintes temporelles (fraîcheur, latence…). La spécification est automatiquement analysée pour montrer sa faisabilité et en dériver une implantation (thèse Tanguy Le Berre 06-).

Un deuxième sujet, en collaboration avec Thales Alenia Space et le CNES, s’attache à la cohérence des données dans des systèmes distribués temps-réel. Dans un tel système, plusieurs chemins de données indépendants peuvent relier deux composants mais le composant terminal peut nécessiter une cohérence globale de ses entrées. Nous avons identifié les points d’incohérence et proposé différentes approches pour contrôler le degré de cohérence (thèse Nadège Pontisso 06-).

Enfin, suite à une demande du CNES en 2007, la notion de séparabilité a été utilisée pour améliorer la simulation de systèmes satellitaires répartis (taille des pas et parallélisme).

Courtage de service

le courtage de service a été étudié en utilisant une description formelle du domaine d’application comportant l’ensemble des données et des opérateurs du domaine ainsi que les propriétés des opérateurs. Cette description est effectuée sous la forme d’une spécification algébrique, intégrant sous-typage et surcharge. Le courtage consiste à effectuer un filtrage modulo la théorie équationnelle associée à la spécification (thèse Aurélie Hurault 03-06 [10732], projet interne GRID-TLSE, collaboration avec l’Arménie, projets ANR LEGO et SCORWARE).

Voir aussi le site de l’équipe Modélisation et Validation de la Répartition à l’IRIT/ENSEEIHT.