GROUPE de RECHERCHE « Systèmes Parallèles et Communicants »  - Rapport Activités 2000

Préambule

Cette « jeune » équipe a été constituée à Marseille depuis cinq ans par apport d'une partie des activités de l'équipe "Systèmes Massivement Parallèles" du laboratoire LGI-IMAG à Grenoble et de l'équipe "Preuve de Circuits" du LIM à Marseille ainsi que des recrutements nouveaux et rapprochement thématique d’enseignants-chercheurs de deux universités marseillaises « Université de la Méditerranée » et « Université de Provence ». 
Dans le processus de "restructuration" (sic!) du laboratoire LIM, certains membres de l’équipe (en italique ci-dessous) ont du rattacher une partie ou la totalité de leurs activités au projet de constitution d’une nouvelle équipe « Modélisation et Vérification » dans le projet de laboratoire LIF ou au projet de laboratoire LSIS.

Composition de l’équipe (2000-2001)

Responsable Scientifique : T. Muntean , Pr. Université de la Méditerranée  (Délégation DR CNRS-Grenoble)
Chercheurs :

Solange COUPET-GRIMAL, MC-Univ. Provence                                             

Cristian ENE, ATER, Univ. Méditerranée
   
   Arnaud FEVRIER, MC-Univ. Méditerranée

Marc GENGLER, PR- Univ. Méditerranée

Line JAKUBIEC, MC- Univ. Méditerranée

Léon MUGWANEZA, MC- Univ. Méditerranée

Traian MUNTEAN, PR- Univ. Méditerranée

Tin NGUYEN, MC- Univ. Méditerranée
       
        Jean-Luc PAILLET, MC(H)- Univ. Provence
       
        Laurence PIERRE, MC(H)- Univ. Provence

                         Marjorie RUSSO, ATER, Univ. Méditerranée


Anciens membres:
R. Amadio (Pr. Univ. Provence); Robert Despons (post-doc); Alba Cristina de Melo (doctorante); Leila Bacouche (doctorante); Harold Castro (doctorant)

 

Doctorants au 1er Octobre 2001

   Ludovic Casset, allocataire CIFRE (GemPlus Labs)

   Javier Garmendia, boursier CNRS+Région PACA, Responsable Start-Up (Beemind)

            Ludmila Klenov, contrat CNRS

            Olivier Rolland, allocataire MESRT

            Hervé Quiroz, contractuel

 

Collaborateurs Extérieurs :    Jean-Raymond ABRIAL (>99)
                                                       Antoine RAUZY, CR1-CNRS (>01)
                                                        Sandrine SAMSO, RTE-EDF, PAST-IUT Univ. de la Méditerranée



Présentation

L’évolution des systèmes informatiques a été marquée ces deux dernières décennies par le développement sans précédent des systèmes et réseaux qui permettent l’interconnexion de stations (e. g. Internet) ou de processeurs par l’apparition des machines dites  d’« architectures parallèles ». Ceci suscite une intense activité de recherche de par le monde autour des applications parallèles et distribuées, des systèmes répartis et communicants et de leurs fondements théoriques. Ces efforts de recherche commencent aujourd’hui à porter leurs fruits, mais le nombre de problèmes ouverts n’en demeure pas moins important. Des problèmes nouveaux ont également émergé par les architectures futures de systèmes communicants et d’exigences nouvelles des applications, (réseau en particulier). Pour que leur évolution et leur utilisation soient ancrées dans des fondements théoriques de conception qui puissent assurer leur correction de fonctionnement et de leur comportement dans divers environnements d’utilisation, des travaux basés sur des principes fondamentaux, génériques,  de construction de tels systèmes restent de la plus grande actualité. C’est dans ce cadre que nos travaux actuels s’inscrivent.

        Thème de recherche :
Dans ce cadre, notre équipe a comme objectif commun de proposer des principes fondamentaux, des méthodes théoriques, des techniques et des outils pour la construction correcte des systèmes communicants, parallèles et distribués (concurrents asynchrones). La correction de ces systèmes est dans notre approche un objectif dans les modèles et les méthodes de spécification et de construction proposées par complémentarité à la preuve a posteriori de leurs propriétés.
Domaines d’applications :
systèmes complexes concurrents et applications coopératives temps critiques, systèmes communicants et embarqués (e.g. pour cartes à puces), télécommunications, communications et agents mobiles, réseaux d’interconnexion

Notre projet scientifique intègre de manière cohérente deux domaines d’expertise complémentaires:

modèles pour le parallélisme, la concurrence et la communication

méthodes formelles et outils pour la spécification, la construction correcte de tels systèmes

La conception des systèmes communicants/distribués et les aspects fondamentaux pour leur construction correcte (par des modèles et méthodes mathématiques appropriés), est donc la thématique principale que notre équipe développe. Ces systèmes sont essentiellement caractérisés par une très bonne adéquation à leurs fonctions de base (s'exécuter correctement et avec les performances requises -qui deviennent ainsi un facteur de correction), tout en présentant une grande adaptabilité d'implémentation (généricité, « scalabilité »). Elle se caractérise souvent par une répartition configurable de leurs composants qui peuvent se trouver naturellement distribués de manière active sur plusieurs sites interconnectés par des systèmes communicants (réseaux, télécoms, etc).

Nos activités actuelles concernent plus précisément les axes de recherche suivants: 

• modèles pour la conception et la programmation de systèmes concurrents asynchrones

• méthodes et mécanismes génériques pour la construction correcte de systèmes communicants hétérogènes– routage, reconfigurabilité, mobilité ; spécification de tels systèmes

• méthodes de construction correcte pour systèmes distribués par raffinements successifs prouvés

Démarche de Collaboration Extérieure

Nos projets se sont concrétisés en général par des collaborations nationales et internationales comme notamment dans le cadre de plusieurs projets européens (e.g. actuellement le projet MATISSE du 5e PCRDT mené au CNRS Grenoble dans le cadre de la délégation de T. Muntean).

Des nombreuses valorisations de recherche et développement en France et à l'étranger issues de nos projets ont permis ces dix dernières années la réalisation d'une vingtaine de contrats d'étude et recherche à Grenoble et depuis 1995 à Marseille.

Nous avons été aussi soucieux de donner à nos travaux une visibilité internationale par des nombreuses collaborations avec des laboratoires étrangers actifs dans ce domaine. Des professeurs ou chercheurs étrangers ont ainsi effectué des périodes sabbatiques ou des séjours dans notre équipe.

Travaux et résultats depuis 1997

Conception correcte de systèmes parallèles : routage, communications et mobilité

Nous nous sommes intéressés depuis une dizaine d’années à la correction des mécanismes de contrôle des communications (acheminement des messages) dans les réseaux d’interconnexion quelconques et l’algorithmique distribuée associée. Notre approche a été basée sur la construction incrémentale de machines virtuelles sur un micro-noyau générique pour supporter correctement divers modèles de programmation parallèles. Dans cette optique, les activités de l'équipe ont été concentrées autour des problèmes posés par la conception d'une architecture nouvelle de noyau de contrôle des communications basé sur des algorithmes corrects de routage et reconfigurabilité.

L'accent a été mis ces dernières années sur des solutions qui se caractérisent par la généricité, l’optimalité et la reconfigurabilité dynamique de tels systèmes (logiciels ou matériels) :

dans les systèmes parallèles (thèses de Christophe Aussagues[A98]) ;

Nous avons développé des algorithmes de routage adaptatifs pour réseaux généraux ([RMM99a], [RMM99b], R 99]). Ces algorithmes utilisent une représentation compacte des informations de routage basée sur une extension originale du routage par intervalles proposée auparavant dans la thèse de Léon Mugwaneza..

Spécification et preuves de systèmes concurrents (L. Pierre, T. Nguyen, T. Muntean)

Après avoir étudié et comparé les avantages et inconvénients de divers langages existants pour la spécification de systèmes réactifs et de systèmes communicants [P97a], Laurence Pierre et Tin Nguyen se sont intéressés à la spécification formelle et à la validation de bibliothèques de primitives de communication [GPN00]. Notre but etait de proposer un ensemble de descriptions formelles pour les primitives nécessaires à la spécification des communications dans les systèmes répartis, et de les valider (par la vérification d'un certain nombre de propriétés temporelles) de façon à fournir une base, d'une part pour la spécification des fonctionnalités plus élaborées, et d'autre part pour la mise en œuvre informatique de ces primitives et fonctionnalités. Nous nous sommes particulièrement concentrés sur le passage de messages dans les programmes de type MIMD. Il etait alors naturel d'utiliser les primitives décrites dans le standard MPI ("Message Passing Interface"). Celui-ci propose toutes les fonctions utilisables dans la réalisation de divers types de communications (point à point, collectives, synchrones ou asynchrones) mais le document de spécification ne donne que des spécifications très informelles, et des interfaces de fonctions C ou Fortran. Nous avons entrepris la définition de spécifications formelles pour certaines de ces primitives, et nous avons choisi pour cela l'un des langages formels les plus largement utilisés pour la description de processus communicants, LOTOS. Par ailleurs, nous avons également spécifié un mécanisme, que nous appelons "gestionnaire de communications", charge de collecter et de satisfaire au mieux les requêtes des processus utilisateur et de gérer certains types d'erreurs. Nous l'avons conçu et réalisé à partir d'informations apparaissant en filigrane dans le document de spécification du standard.

Enfin, grâce au model checker intégré a CADP, environnement spécialisé pour le développement de descriptions LOTOS conçu a Grenoble, nous avons réalisé la vérification de propriétés temporelles exprimées en mu-calcul sur certains de nos modèles (i.e. les modèles finis uniquement, seuls manipulables par l'outil utilise).

Par ailleurs les travaux conduits auparavant par Laurence Pierre dans ce même thème concernent :

Descriptions VHDL comportementales.

Il s'agit de travaux réalisés dans le cadre de la thèse de F.Nicoli. L'objectif a été de pouvoir raisonner sur un ensemble aussi large que possible de descriptions VHDL comportementales, synchrones ou asynchrones. Le formalisme utilisé se présente comme une fonction récursive symbolisant la répétition du cycle de simulation sur une "architecture" VHDL. La preuve se fait par analyse des traces de simulation. Le problème qui se pose alors est de savoir dans quelle mesure de telles "traces de simulation" peuvent permettre d'identifier des circuits équivalents.

Architectures répétitives génériques.

Nous nous concentrons ici sur les architectures répétitives paramétrées par la taille des vecteurs manipulés. Une telle architecture correspond, dans le style structurel de VHDL, à une description générique itérative. Ce travail se poursuit actuellement dans le cadre de la thèse d'E.Gascard par un style de modélisation base sur les graphes de Cayley ([GP98]). Notre objectif est de déterminer si une telle approche peut être plus intéressante que les modèles récursifs. Les graphes de Cayley donnent une représentation des groupes mathématiques, et en particulier des groupes de permutations. A ce titre, ils sont souvent utilisés pour modéliser les réseaux d'interconnexion symétriques (tore, hypercube,...) dans des domaines comme la recherche de bons algorithmes de routage, la tolérance aux pannes,...

Descriptions comportementales synchrones avant et après synthèse.

Il s'agit d'un travail assez récent réalisé en collaboration avec D.Borrione et J.Dushina (laboratoire TIMA, Grenoble) qui concerne la définition d'une formalisation mathématique des modèles utilisés pour la validation de descriptions VHDL obtenues par un processus de synthèse de haut niveau. Nous avons proposé une formalisation du modèle de FSMD introduit par Gajski, ainsi que de l'interconnexion des parties contrôle/operative après synthèse, dans le cas ou la partie operative est purement combinatoire ([P97b], [BDP98], [BDP00]).

Systèmes synchrones et asynchrones

Les systèmes matériels synchrones réalisent un comportement ayant une part importante de parallélisme inhérent à la structure, qui est très commodément modélisé dans un style de langage fonctionnel. C'est dans ce but qui a été défini initialement le système formel P-calcul dont les expressions du langage correspondent aux interconnexions de composants, et dont la sémantique, exprimée par une algèbre fonctionnelle [ACP96] correspond aux comportements synchrones. Le P-Calcul est donc une méthode de spécification, indépendante des divers outils de preuve formelle utilisés dans la conception d'un système donné.

Le travaux autour de ce sujet ont été sur deux thèmes:

• Spécifications multi-niveaux de systèmes : nous avons étendu l'algèbre fonctionnelle P-calcul, de manière à pouvoir spécifier formellement des systèmes en partant d'un très haut niveau d'abstraction et sans supposer la nature de l'implémentation cible. Les niveaux inférieurs de spécification sont obtenus par des raffinements successifs, définis par des horloges "logiques" de plus en plus fines. Pour cela, nous avons rajouté au modèle initial des opérateurs de changements d'échelle temporelle, ce qui donne une nouvelle algèbre fonctionnelle: le tau-calcul. Le principe, utilisé ici, de découpages successifs du temps, suppose un modèle de temps synchrone ou pseudo-synchrone (horloge logique), et donc que les systèmes modélisés peuvent se synchroniser avec leur environnement. (J-L. Paillet en collaboration avec T.Muntean [PM99]).

• Spécifications formelles pour les systèmes temps critiques asynchrones (J-L Paillet et thèse W. Jumpamule): notre motivation a été de fournir à des non spécialistes, une méthode de spécification formelle de haut niveau [GJP99] qui soit simple et qui utilise des concepts les plus proches possibles d'une description informelle, tout en permettant 

- d'une part , d'obtenir par traduction dans un langage de description plus détaillé, tel que le modèle à états DEVS (Discrete Event Systems), des objets simulables avec toute la précision temporelle souhaitée

- d'autre part, d'effectuer des vérifications de cohérence formelle préalables à toute simulation.

Analyse et transformations de systèmes communicants (M. Gengler, M. Martel, T. Muntean)

L'analyse des programmes séquentiels a pour but d'expliciter le parallélisme et d'optimiser la gestion de données. L'analyse de programmes parallèles vise à simplifier par transformations prouvées les programmes (simplification des communications) en tenant compte d'informations sur les données [MG00b]. Elle s'apparente donc au problème d'évaluation partielle.

En un premier temps, nous avons décrit, par le biais du pi-calcul [GM97], un noyau de communication dans les programmes parallèles et montré la correction des transformations d'un programme correctement annoté. Nous avons construit une fonction d'annotation des programmes par analyse du programme pour décrire les communications possibles lors de son exécution, ainsi que les données transmises lors de ces communications (thèse de Matthieu Martel [M00], [GM98]). Il s'agit aussi de donner des approximations, aussi fidèles que possibles, des communications qui seront possibles pendant l'exécution, ainsi que des données transmises.

Les lois de transformation automatique pour un modèle de processus à diffusion sont développées dans les travaux de thèse de Cristian Ene [EM01].

Outils d'aide à la démonstration automatique de systèmes (S. Coupet, L. Jakubiec, T. Muntean, J-L. Paillet)

Notre activité se situe dans le cadre de la spécification et la preuve formelle de systèmes informatiques.  Le coût élevé des techniques de test ou de simulation, qui, de plus, ne sont pas exhaustives, a conduit bon nombre d'industriels et d'universitaires à utiliser de plus en plus largement les méthodes formelles et à étudier divers langages de spécification, systèmes formels, logiques. Parallèlement, s'est révélée la nécessité d'utiliser des outils informatiques d'aide à la preuve pour vérifier la consistance des spécifications et la validité des démonstrations mathématiques. C'est ainsi que nous avons axé ces dernières années notre travail de recherche sur la spécification et la vérification en liaison avec des systèmes automatisés  d'aide à la preuve.

Modélisation de systèmes matériels synchrones (S. Coupet, J-L Paillet)

Les systèmes matériels synchrones ont une part importante de parallélisme inhérent à la structure, qui est très commodément modélisée dans un style de langage fonctionnel. Avec Jean-Luc Paillet et Michel Allemand, nous avons entièrement décrit et fondé un système formel, le P-calcul dont les expressions du langage correspondent aux interconnexions de composants, et dont la sémantique, exprimée par une algèbre, correspond aux comportements synchrones fonctionnels ([ACP96], [ACJP96], [JCC97]).

Correction de systèmes distribués. (S. Coupet, L. Jakubiec, T. Muntean)

Notre étude a aussi porté sur les systèmes parallèles et communicants. Nous avons en particulier spécifié dans le calcul des constructions enrichi de définitions co-inductives, les différentes notions d'équivalence et de congruence pour les systèmes de transitions étiquetés sous-jacents aux algèbres de processus. On y utilise largement les types co-inductifs, pour raisonner sur des plus grands points fixes. Ce travail fait partie de la distribution COQ [C].  Avec Cristian Ene et Traian Muntean, nous avons étudié une spécification de Occam en Coq, en vue de construire des systèmes parallèles par transformations formelles certifiées.

Types dépendants et systèmes de numération (S. Coupet, L. Jakubiec)

Nous nous sommes penchés sur les méthodes de  spécification avec types dépendants qui permettent des descriptions très précises, donc très fiables. En revanche, ils induisent des problèmes logiques difficiles. On ne peut, par exemple, exprimer  l'égalité de deux objets dont les types dépendent de termes distincts même quand on a prouvé que ces termes vérifient l'égalité de Leibniz. Nous avons produit, dans le cadre de cette étude, une axiomatisation très complète des listes dépendantes puis des systèmes de numération, sur laquelle nous nous appuyons pour vérifier toute une classe de circuits arithmétiques linéaires [CJ96]. Ce travail fait partie de la distribution COQ [CJ]

L'utilisation des types co-inductifs introduits dans Coq par Eduardo Gimenez a amené Solange Coupet, en collaboration avec Roberto Amadio, à s'intéresser aux déclarations récursives d'objets infinis en théorie des types. Dans [AC98], nous avons proposé une interprétation des types co-inductifs basée sur des relations d'équivalence partielles dont on peut extraire des règles de typage pour ces définitions récursives.

Automates et applications (S. Coupet, L. Jakubiec)

Nous avons donné une axiomatisation des automates de Moore et de Mealy basée sur des règles de composition algébriques et des équivalences d'automates et avons produit diverses preuves de congruence. Nous avons largement utilisé l'ordre supérieur, ainsi que les définitions par plus grand point fixe et les types co-inductifs pour modéliser les flux infinis en entrée et en sortie des automates. Nous nous sommes appuyés sur cette étude pour donner, en vue de leur vérification, une description uniforme des circuits synchrones décrits au niveau transfert de registres et de leur comportement. La preuve qu'un circuit est correct revient à prouver sous certaines pré-conditions une équivalence entre automate structurel et automate comportemental. C'est l'objet d'un lemme générique prouvé co-inductivement. Ce résultat est fondamental car il capture tout l'aspect temporel des preuves de correction des circuits séquentiels synchrones. Enfin, nous avons mené une étude de faisabilité en appliquant notre méthodologie à la preuve d'un circuit de taille et de complexité significatives. Il s'agit du Fairisle ATM Switch Fabric réalisé à l'Université de Cambridge. C'est une partie d'un réseau ayant un mode de transfert asynchrone et le Switch Fabric est l'élément d'aiguillage des données. Notre approche est hiérarchique et modulaire et la vérification se fait par instanciation des fonctions et des lemmes issus de nos bibliothèques générales ([GJ99, Thèse Line Jakubiec [J99], [JCC97]).




Projet de Recherche : Méthodologie de Construction Correcte pour Systèmes Critiques Communicants

Présentation

Pour réaliser des logiciels parallèles/distribués on pourrait se contenter d'une approche pragmatique classique (spécification, conception, codage, tests réalisés dans le cadre d'un processus de génie logiciel), qui a déjà fait ses preuves. Depuis bien des années, en effet, le génie logiciel a connu et mis en œuvre un certain nombre de théories, de pratiques et d'outils qui ont visé (et souvent très bien réussi) à une certaine rationalisation et systématisation de la pratique du développement logiciel. Plus récemment, ces pratiques se sont vues adjoindre (surtout en matière de développement matériel et dans une moindre mesure du logiciel) des techniques très prometteuses de « synthèse automatique ».

Mais toutes ces techniques ne sont actuellement plus suffisantes au regard des exigences de correction et qualité que l'on souhaite atteindre sur les systèmes concurrents complexes (souvent ouverts et hybrides ou hétérogènes). En effet, si ces techniques visent à augmenter considérablement le soin que l'on peut apporter au développement des logiciels, elles n'en changent pas fondamentalement l'approche, qui reste en définitive extrêmement pragmatique et "intuitive". Dans la grande majorité des cas, le système est d'abord construit et l'on vérifie ensuite (et a posteriori seulement) qu'il possède bien, ou est conforme, à un certain nombre de propriétés souhaitables (vérification, validation, tests de conformité).

Il est certain que certaines disciplines scientifiques qui sont à la base de technologies plus "mûres" (aéronautique, nucléaire, génie civil, etc) ne procèdent pas de cette façon. Il est clair que l'on ne construit pas un avion pour vérifier ensuite qu'il vole bien ; on le construit essentiellement en ayant en permanence à l'esprit (depuis le début de sa conception jusqu'à sa réalisation finale) qu'il doit voler suivant certains paramètres ou lois et cette propriété est constamment "prouvée" et totalement "intégrée" au processus de réalisation à tous les niveaux.

Le cadre de notre projet suit une approche de construction système plutôt que preuve de programmes. La réalisation des systèmes informatiques distribués complexes tombe, pour beaucoup de cas applicatifs (contrôle commande distribuée, télécommunications, cartes à puces, robotique mobile) dans les descriptions que nous venons d'esquisser. En particulier, on peut constater que certains formalismes ne sont souvent utilisés dans le processus de développement de ces systèmes que pour décrire de façon plus ou moins abstraite ce que l'on veut construire (langages de spécification), mais pas pour raisonner sur les propriétés à respecter tout au long du processus de construction comme par exemple des contraintes de distribution et de parallélisme (contraintes de communication/synchronisation, localité, mobilité) inhérentes à la classe de systèmes construits. C'est pourtant ce type de caractéristiques qui gouverneront impérativement la correction d'un tel système. 

Une caractéristique architecturale de ces systèmes est donc l'utilisation inhérente du parallélisme et de la distribution, avec des contraintes d'extensibilité, d'ouverture et d'hétérogénéité comme principes de base de conception dès la phase de spécification fonctionnelle et même, à plus haut niveau, lors de la constitution du "cahier de charge" associé.

A la différence d'une approche pragmatique, la complexité croissante des systèmes précités rend de plus en plus souhaitable, voire indispensable, l'utilisation de lois et de méthodes formelles tout au long du processus de conception et pas uniquement pour la vérification/validation a posteriori. Très peu de méthodes formelles ont été utilisées pour le développement rigoureux et systématique d'applications complexes et encore moins de manière "constructiviste" (depuis la spécification de haut niveau jusqu'à la génération automatique ou la réalisation des programmes/circuits qui les implémentent). Par exemple, la "Méthode B" d’Abrial, ou encore le modèle FDR issu de CSP (Université d’Oxford), ou les « action systems » (Université de Turku) ont pour  ambition de fournir un cadre conceptuel et des mécanismes aptes à servir à la mise en œuvre de la construction correcte et prouvée d'un système.  Celui-ci est d'abord défini par les propriétés qu'il doit satisfaire, et ce de façon relativement abstraite ; ces propriétés sont ensuite spécifiquement affinées (davantage de détails du système sont pris en compte dans un processus formel de transformation par des lois prouvées de "raffinement"), puis le système est enfin construit, là encore par raffinements successifs. La preuve formelle des raffinements accompagne ici l'ensemble du développement. Notre projet de recherche s'inscrit actuellement dans le cadre des méthodes de conception correcte de systèmes de cette classe et la réalisation d'outils pour la programmation et/ou le contrôle des systèmes parallèles/distribués communicants complexes. La construction des tels systèmes (souvent critiques pour les applications informatiques) a pris une  importance économique et stratégique accrue et les exemples applicatifs sont nombreux.

L'utilisation pratique d'une telle approche, bien que limitée actuellement à certaines applications, pour des applications réelles est assez récente, mais toutefois avec une certaine avance en Europe (e.g.. l'utilisation de la Méthode B pour le projet de ligne de métro à conduite entièrement automatique, ou l’utilisation de FDR de Formal Systems pour le co-design et également pour certains logiciels de contrôle ou protocoles sécurisés développés au DERA en GB). Le logiciel ou le système n'a plus à être validé après-coup, bien qu'il puisse être utile pour certains aspects comportementaux dans des environnements particuliers de le valider/tester aussi; le processus même de construction garantira (par des preuves reproductibles) que le produit final (code généré) respecte bien les propriétés caractéristiques qui ont été retenues au début de la conception, mais possède aussi celles, souvent liée dans les systèmes actuels aux contraintes de distribution et/ou parallélisme, rajoutées  au cours du processus de raffinement pour l’implémentation finale.  Ces phases en amont ont pour but de déterminer la viabilité et  les caractéristiques optimales du système que l'on veut construire (performances, configurations, sécurité et sûreté).

Notre projet, qui a été à la base d’une proposition contractée par le CNRS dans le cadre du programme IST du 5e PCRDT, « MATISSE », qui se déroule en collaboration permanente avec plusieurs équipes R&D industrielles (en France avec GEMPLUS, MATRA-MTI,  STERIA), nous proposons d'approfondir une telle démarche pour la conception correcte de systèmes communicants critiques et aussi de valider, sur des cas précis de systèmes et d'applications pilotes fournies par nos partenaires industriels, ce type d'approche. Le projet comporte des applications et études de cas  proposées par GEMPLUS (multi-applications smartcards, machines virtuelles et supports noyau embarqués pour cartes à puces-JavaCardVM) ou par Matra-MTI  (contrôle automatisé distribué pour réseaux ferroviaires). Des travaux communs et en collaboration (thèses de doctorat, conventions) ont déjà commencé depuis deux ans dans le cadre de ce projet.

Approche proposée et objectifs

Nos objectifs plus spécifiques sont liés aux problèmes inhérents à la conception correcte des systèmes concurrents ou des systèmes communicants, pour lesquels le comportement attendu peut varier en fonction des conditions d'utilisation dans divers environnements applicatifs et dans le temps. Les interactions entre les composants, la localisation même des composants ainsi que leur modèles de programmation et architectural sont des sources importantes de problèmes nouveaux. Contrairement aux modèles statiques utilisés le plus souvent par le passé, des modèles dynamiques seront utiles pour des applications (par exemple, des réseaux configurables, agents actifs mobiles, communications adaptatives). 

La complexité inhérente des tels systèmes, le nombre de cas possibles, qu'il faudrait analyser pour spécifier, construire et raisonner sur leurs comportements souvent non-détérministe, est très important et nécessite un développement rigoureux, contrôlé de manière précise à toutes les étapes de conception et de réalisation.  De surcroît, la distribution et l'évolution souvent dynamique de ces systèmes rajoutent un degré de complexité, car les différentes parties des logiciels peuvent opérer plus ou moins indépendamment.  Il nous paraît important donc que des modèles architecturaux et de programmation adéquats ainsi que des méthodes formelles appropriées doivent être utilisés pour la conception et la preuve comportementale de ces systèmes, lors du processus de construction et d’implantation même.

L'originalité du projet est donc double :

• il s'agit, d'une part, de prendre en compte le parallélisme et la distribution dès les premières phases dans le processus de raffinement lors de la construction par transformations successives prouvées des comportements du système. 

• d'autre part, il faut accompagner le processus de construction correcte par des  propriétés d'optimalité et et de généricité dans toutes les phases du processus  de raffinement.

Dans ce projet l’approche "constructiviste" est appliquée pour la conception correcte de tels systèmes, parmi lesquels notre projet s’intéresse, en particulier, aux logiciels et systèmes critiques de communication (systèmes d’objets mobiles et à diffusion, routeurs adaptatifs corrects), aux micro-noyaux de contrôle de la concurrence et/ou de la mobilité utilisés dans les applications (télécommunications, cartes à puces) ou encore des machines virtuelles génériques multi-applications.

L'aspect constructiviste comporte deux caractéristiques essentielles: 

• la construction des systèmes est incrémentale, obtenue par raffinements parallèles successifs, 

• des preuves (automatisables) sont utilisées tout au long du processus de développement des logiciels ou des systèmes et leur configuration. 

 

Le parallélisme et les interactions, la localisation des composants et leur mobilité (voire la transparence de la localisation) rajoutent un niveau de complexité à la spécification. Il s'agit d'abord de spécifier les composants et leurs interactions, pour ensuite les raffiner et les configurer ou distribuer correctement ou de manière optimale. Ceci peut, par exemple, vouloir dire qu'un composant vu comme un monolithe à un certain niveau d’abstraction se retrouve instancié par un ensemble de composants dont le comportement est plus simples à prouver ainsi que leurs interactions à un niveau d’implémentation réel. De même, une interaction (ou un protocole sécurisé) pourra éventuellement être raffinée en un message qui utilise un encryptage, suivi d'un message d'acquittement, le tout faisant peut-être intervenir un contrôleur qui veille à l'ordonnancement correct de l'ensemble des messages échangés ou à la sécurité ou la sûreté des échanges.

Le principe de preuve de tels raffinements de composants parallèles suit les mêmes grandes lignes que dans le monde séquentiel mais la preuve de correction doit intégrer les interactions. Il s'agit de s'assurer que les propriétés initialement exigées sont préservées. A titres d'illustration, il faudra montrer que l'observabilité du système ne change pas pour un observateur externe, que l'ordre logique des messages ou l'ordre causal sont préservés, que la mobilité des processus réels est masquée si nécessaire par un mécanisme de transparence de localisation, ou encore que les propriétés comme la vivacité ou la terminaison sont des invariants à tout niveau d’abstraction. Ce type de contraintes est proche de ceux que nous connaissons déjà pour analyser des programmes parallèles ou pour raisonner sur eux. Plutôt que de franchir en un seul pas le "gap" entre un programme et sa spécification ou description fonctionnelle de haut niveau, nous utiliserons de nombreux niveaux de raffinement intermédiaires automatisables et factorisables autant que possible.

La Méthode B, ou FDR, particulièrement bien adaptés à une telle approche constructiviste et l'utilisation d’outils appropriés ainsi que les collaborations avec Matra-MTI et Gemplus Labs pour une classe importante de systèmes critiques nous permettent de donner à ce projet un aspect de valorisation important, dès les premières phases.

Les bénéfices de ce projet sont multiples. Les premiers concernent, bien sûr, l'étude de faisabilité d'une telle approche ainsi que l'acquisition de la maîtrise des techniques dans le domaine de la construction correcte des systèmes critiques communicants pour des grandes classes d'applications.  Un autre résultat très important concerne l’évolution des méthodologies et des outils utilisés pour mettre en œuvre cette approche dans divers domaines d'applications (systèmes pour cartes à puces, machines virtuelles et noyaux intégrés pour applets mobiles, contrôleurs distribués embarqués).

Nous pensons, comme nous l'avons déjà démontré dans d'autres projets, que le succès des réalisations pratiques dans ces domaines de technologie avancée ne peut être obtenu qu'au prix d'une étroite symbiose tout au long du projet entre les divers acteurs: chercheurs, industriels et utilisateurs. Cette symbiose a été recherchée et réalisée dans ce projet dès le début ; le projet européen MATISSE en témoigne.  A plus long terme, dans le domaine de la construction correcte proprement dite et surtout de sa mécanisation (l'automatisation la plus grande est évidemment le but recherché), ce projet nous montrera s'il existe des techniques de preuve, ou tout au moins des théories fréquemment utilisées, qu'il soit nécessaire de rendre génériques dans les outils de génie système.  De telles méthodologies offrent l'avantage de capitaliser un savoir-faire permettant de développer rapidement, et de manière sûre, des applications similaires, comme ceci commence à se faire de par le monde dans divers domaines d'applications critiques (transport, réseaux, télécommunications, accès sécurisés…).

 


Actions de recherche en cours

Modèle algébrique pour systèmes communicants à diffusion

Participants : Cristian Ené, Traian Muntean , Diana Toma

Nous développons un modèle de calcul de processus (en extension à CBS et ∏-calcul) pour les systèmes reconfigurables qui utilise la diffusion comme primitive de base de communication et nous proposons une sémantique opérationnelle pour ce calcul [EM99, EM00]. Ceci nous permet de raisonner sur les systèmes à diffusion et leurs applications grâce à trois types de relations d’équivalence comportementale introduites (thèse de C. Ené en cours). Un résultat important de ce travail est que ces relations peuvent coïncider en fonctions de différentes voies pour traiter l’équivalence/non-équivalence de deux systèmes. On donne dans [EM00] une axiomatisation complète et le travail en cours consiste à modéliser des classes d’applications rencontrées en télécommunications mobiles, réseaux.

Routage et Mobilité dans les systèmes communicants

Participants :  Javier Garmendia, Léon Mugwaneza, Traian Muntean

Le travail sur le routage adaptatif et la mobilité se poursuit sur deux aspects :

• Le routage dans les systèmes à processus mobiles :

De plus en plus d’ applications sont basées sur le paradigme des processus (ou agents) mobiles. Dans ce modèle, les processus changent de localisation soit pour offrir un nouveau service, soit pour améliorer les performances. Dans les systèmes supportant les processus mobiles, le contrôle des communications devient plus complexe du fait de la mobilité des sources et destinataires. L’utilisation des techniques classiques basées sur l’adresse de la machine hôte peut conduire à des solutions inefficaces dans le cas où les processus « migrent » souvent. Pour tenir compte de la mobilité des processus, nous avons proposé une nouvelle technique de routage, appelé Pi-routage, qui tient compte, dans les informations de routage, de l’identification du processus ([GRMM00]) J. Garmendia, S.Rivas, L Mugwaneza, T. Muntean)

Des mises à jour dynamiques des tables de routage lors des migrations des processus, permettent de rediriger les messages vers la nouvelle localisation du destinataire sans avoir à passer par l’ancienne localisation. Notre solution est actuellement en cours d’évaluation tant sur les techniques de nommage des processus, que pour les algorithmes de mise à jour des informations de routage.

 

• Noyau de routage support pour la diffusion

Nous sommes en particulier intéressés par la construction de mécanismes pour supporter des schémas de communication à diffusion et leur correction [GNP00] et aussi aux algorithmes de routage compactés associés (thèse J. Garmendia en cours).

Modèles formels pour les systèmes ouverts distribués

Participants : Arnaud Février, Léon Mugwaneza, Tin Nguyen

L'axe de recherche se situe dans  le contexte  des applications de télécommunications. Les  opérateurs s'orientent vers des développements de nouveaux services qui utilisent des systèmes à objets distribués: ODP,  TINA,  CORBA, OMG ; pour applications  multimédia,  systèmes temps critique, collecticiel.

Nous nous intéressons particulièrement à la conception correcte d'un système ouvert à objets interopérants pour lesquels la gestion de la qualité de service est critique. Ces systèmes regroupent en particulier des protocoles et noyaux de communications, les flux multimédia et les définitions des comportements des nouveaux services de télécommunication. L'administration des réseaux de télécommunication (IP, ATM, OSI) est à cet égard intéressante tant pour l'utilisation et comme sujet d'étude pour les problèmes nouveaux posés. Le but des recherches est de proposer des extensions pour les modèles à objets et temps critique. Ces travaux s'appuieront sur des réalisations pratiques sur des plates-formes à objets distribués (java //, CORBA) d'applications de collecticiels par exemple.

Dans le cadre du projet Matisse nous étudierons l’application de la Méthode B pour construire des applications CORBA. Cet axe donne lieu à des collaborations avec des centres de recherches publics (CPqD) et industriels (EDF, Bouygues Télécom).

Interactionsdans les systèmes concurrents

Participants : Laurence Pierre, T. Muntean

Dans la conception des systèmes concurrents communicants, il est essentiel de garantir divers aspects liés aux interactions entre les processus : conception fonctionnelle correcte, absence de blocages, réalisation espérée des communications, sécurité dans les communications, etc... Dans ce cadre, l'utilisation des méthodes formelles fournit une alternative intéressante et fiable aux techniques de type simulation ou test. Elle repose d'une part sur la définition de méthodologies de spécification formelle, et d'autre part sur la mise en œuvre de techniques de preuve associées. Ces techniques peuvent notamment s'apparenter à la démonstration automatique au sens général du terme (application d'outils de type démonstrateurs de théorèmes ou assistants de preuve) ou au model checking. Dans ce thème, nos activités concernent la spécification formelle mais également la preuve, essentiellement du point de vue model checking.

Dans le cadre du projet exposé ci-dessus, nous nous intéressons actuellement aux aspects liés à la sécurité dans les systèmes concurrents communicants. En effet, dans les applications logicielles de type applications pour cartes à puces, il est primordial de garantir l'absence de vulnérabilité, c'est à dire l'absence de situations dans lesquelles une application pourrait communiquer des informations confidentielles à d'autres applications sur la carte ou au monde extérieur. Dans ce but, des techniques de model checking peuvent également être mises en œuvre.

Le comportement de l'application en ce qui concerne ses interactions avec les autres processus doit alors être spécifié formellement, les situations dangereuses également, et la preuve consiste à s'assurer que ces situations sont incompatibles avec le comportement spécifié. Nous envisageons donc d'utiliser une approche dans laquelle les spécifications formelles seraient réalisées dans un langage comme CSP, langage base sur une algèbre de processus et traces comportementales, et un outil de preuve approprié serait utilisé pour les preuves. Le système FDR, développé à Oxford, qui permet de raisonner sur des spécifications CSP est un bon candidat pour ce genre de réalisation. Le problème consiste alors à décrire les situations de vulnérabilité, à identifier celles qui sont traitables au moyen des techniques de preuve disponibles. Pour les situations dont les caractéristiques dépassent les capacités des outils existants (FDR ou autres), par exemple des descriptions correspondant à des modèles infinis, d'autres moyens de preuve devront être développés. Ce travail se fait en collaboration avec Gemplus, dans le cadre du projet MATISSE.

Extensions des méthodes formelles de raffinement

Participants :  M. Gengler, Lioudmila Klenov, T. Muntean, Laurence Pierre,  Olivier Rolland

Les projets de recherche en cours portent sur:

• Raffinement distribué

Depuis les travaux initiaux de Back (années 80) sur un calcul de raffinements, beaucoup de travaux ont été poursuivis pour dériver correctement des logiciels par raffinements successifs. Abrial a proposé récemment de prendre en compte la distribution en donnant une interprétation opérationnelle des commandes gardées. Butler et Walden  ont démontré comment le raffinement dans les systèmes d’actions (la distribution est inhérente) peut être fait suivant la méthode d’Abrial. Roscoe a introduit une méthode de raffinement pour le modèle CSP de Hoare.

Notre travail dans ce projet (thèse de Olivier Rolland, [RM00] propose d’intégrer la distribution dans les communications (synchrones ou asynchrones) entre « machines abstraites » dans les opérateurs de raffinement même. Ceci permet de construire des machines abstraites parallèles directement à tous les niveaux de raffinement et non de distribuer « à la main » une machine abstraite obtenue par le raffinement « classique ». La prise en compte de la correction des interactions entre les machines abstraites à tous les niveaux de raffinement permet de raisonner sur la correction d’un système globalement (processus communicants et les objets de communication induits) dans le processus de construction.

Raffinement des structures de contrôle et d’exécution itératives

L'amélioration des outils exige la plupart du temps des adaptations ou des extensions au niveau du modèle, qui se retrouvent ensuite concrétisés soit par des extensions des outils (Atelier B) ou des simplifications dans leur utilisation. Une demande importante chez les utilisateurs concerne, à titre d'exemple, la possibilité d'utiliser des structures itératives abstraites à tous les niveaux de la spécification. A l'heure actuelle, ceci est uniquement possible par des artifices d'encapsulation qui limitent les possibilités de raffinement.

Au niveau du modèle, notre étude analyse la notion même de boucle abstraite, ainsi que le sens que l'on peut donner à des raffinements de boucles abstraites. Ensuite, nous déduisons les obligations de preuve induites par ces raffinements et nous les ramenons à leur forme la plus simple affin de garantir un traitement efficace.

Construction Correcte de Systèmes Embarqués pour Cartes Blanches

Participants : Ludovic Casset, T. Muntean (collaboration Equipe Gemplus Labs – Jean-Louis Lannet)

Le concept de carte blanche, contrairement aux cartes à puces « traditionnelles », introduit la possibilité de fournir aux concepteurs d’applications une carte à puces avec uniquement son système d’exploitation embarqué. Accessoirement une machine virtuelle peut être résidente ou bien chargée lors de la première utilisation en fonction de l’application chargée. L’utilisateur charge à sa demande les applications et/ou les machines virtuelles nécessaires via un réseau non sécurisé. La carte doit donc assurer seule sa propre sécurité. L’approche défensive qui consiste à effectuer des tests à chaque pas d’exécution est rendu possible par l’utilisation de la machine virtuelle. Cependant les performances en taille et temps d’exécution ne sont pas compatibles avec les applications cartes à puce.

Deux techniques ont été étudiées pour palier à ces défauts : Proof Carrying Code (PCC) et Typed Assembly Language (TAL). La technique PCC consiste à élaborer hors carte une preuve et à la vérifier dans la carte. Cette preuve peut porter sur un pré-calcul d’information de typage permettant d’éviter un parcours arborescent dans la carte. Dans TAL, des informations de typage supplémentaires (annotation de code natif) sont fournies avec le code et facilitent la vérification par un type checker. Ces deux techniques présentent plusieurs inconvénients; pour PCC, la taille de la preuve est plus grande que le code à vérifier lui même, ce qui pose des problème de taille mémoire. Pour TAL, l’utilisation de code natif complexifie le type checker. Le PCC n’est actuellement pas utilisable sur le langage Java choisi par le standard JavaCard à cause de la taille trop importante de la preuve. Deux solutions sont alors envisageables. La première est de travailler sur l’optimisation de la preuve affin de diminuer sa taille tout en s’assurant que le service est toujours optimal. La deuxième solution est de s’orienter vers un autre langage, plus simple et dont la taille de la preuve est réduite de part la conception même du langage. 

L’objectif de ce travail (thèse CIFRE de Ludovic Casset en collaboration avec Gemplus Labs) est la construction d’un noyau de système embarqué de vulnérabilité de code mobile pour applications JavaCard.

 

 



Publications de l’Equipe (depuis 1997)

 

Livres, Revues, Conférences avec Comité et Actes

 

[EM02]        C. Ene, T. Muntean

                   Testing theories for broadcasting processes, (accepted for publication IDPCS))
     
    
[EM01]        C. Ene, T. Muntean

                   A broadcast based calculus for communicating systems,

                    Proc. of Int. Conf. On Formal Methods for Parallel Programming Technics and Aapplications,

                   IEEE-FMPPTA’01, San Francisco

[BDJSM01] G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Melo de Sousa

                   A Formal Executable Semantics of the JavaCard Platform,

                   Proceedings  ESOP'01, LNCS, Springer-Verlag, D. Sands (ed)

[MGR00]     T. Muntean, J. Garmendia, S. Rivas

                   A Routing Model for Mobile Agents

                   Proceedings of Parallel and Distributed Computing and Systems (PDCS’00,

                   ACM-IASTED Conf. Las Vegas, Nov. 2000

                   http://www.iasted.com/conferences/2000/lasvegas/prog-321.htm

 [RMGM00] S. Rivas, J. Garmendia, L. Mugwaneza, T, Muntean

                   Compact and Correct Adaptaive Routing for General Networks

                   Communication Networks, Distributed Systems Modeling and Simulation,

                   CNDS-WMConf.2000, San Diego, Jan. 2000. http://www.scs.org/confernc/wmc00/text/cnds.html

 [BDJSM00] G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Melo de Sousa

                   Formalization in Coq of the Java  Card  Virtual Machine

          Proceedings of FTfJP'00--ECOOP Workshop on Formal Techniques for Java Programs,

          LNCS, Springer-Verlag,, S. Drossopoulou &al (eds)

[BDP00]      D.Borrione, J.Dushina, L.Pierre

                   A Compositional Model for the Functional Verification of High-Level Synthesis Results.

                   IEEE Transactions on VLSI Systems, Volume 8 (5), October 2000.

[DDGV00]  A. Darte, C. Diderich, M. Gengler, F. Vivien

                   Scheduling the Computations of a Loop Nest with Respect to a Given Mapping

                   Proc. EUROPAR Conf., Munich Sept. 2000

[GRMM00] J. Garmendia, S.Rivas, L Mugwaneza, T. Muntean

                   Pi-routage: une technique d'acheminement des communications pour processus mobiles

                   Renpar'12, Juin 2000, Besancon, http://www.renpar.org/

[GPG00]      P.Georgelin, L.Pierre, T. Nguyen:

                   A Formal Approach for the Specification of Communications in Distributed Systems

                            Proc. 13th Int. Conference on Parallel and Distributed Computing Systems (PDCS'2000)      

                            Las Vegas, August 2000, ISCA

[MG00a]      M. Martel, M. Gengler

                   Analyse statique pour la sûreté des applications distribuées, RenPar12, Juin 2000, Besancon

[MG00b]      M. Martel, M. Gengler

                   Communication Topology Analysis for Concurrent Programs, Proc. SPIN’2000, LNCS-1885

 [P00a]        L.Pierre

                   Induction-Oriented Verification of Replicated Architectures Described in VHDL

                   Journal of Circuits, Systems and Computers,Volume 10 (3 & 4), 2000.

[RCG00]      A. Requet, L. Casset, G. Grimaud, Proof of FACADE verification algorithm using the B Method

                   Proc. of HASE’2000 Conf., Albuquerque, USA, Oct. 2000

[ADT99]     C. Aussagues, V. David, T. Muntean

                   A timeliness model for time critical parallel systems

                   Intern. Conf. on Paralle and Distributed Processing Techniques and Applications

[P99]           L.Pierre & T.Kropt (Eds)

                   Correct Hardware Design and Verification Methods, LNCS 1703, Springer-Verlag, 1999.

                   Las Vegas, IEEE Press Feb.99 (PDPTA’99)

[CJ99]         S. Coupet-Grimal, L. Jakubiec

                   Hardware Verification using Co-induction in Coq, TPHOLs'99

                   Springer-Verlag LNCS 1690, 14-17th September 1999 Nice     

 [EM99]       C. Ene, T. Muntean

                   On the expressive power of point-to-point and broadcast communications

                   Foundations of Theoretical Computing, Springer-Verlag LNCS-Sept.99

[GJP99]       N.Giambiasi, W.Jumpamule, J.L.Paillet

                   High Level Specification of Control Systems: Validation by Simulation

                   CARS&FOF'99, Bresil, Août 99.

[KN99]        R. Kamdem, P. Njiwoua

                    Galois Lattice approach to hardware/software partitioning

                   Intern. Conf. on Paralle and Distributed Processing Techniques and Applications

                   Las Vegas, IEEE Press Feb.99 (PDPTA’99)

[PM99]        J.L Paillet, T. Muntean

                   t--calculus, A Multilevel Specification and Design Methodology for Reliable Systems

                   HighSys’99 Conf. on High Reliable Hardware and Software Systems München, Oct.99

[RMM99a]    S. Rivas, L. Mugwaneza, T. Muntean

                   Application  d'un algorithme de routage adaptatif au tore bi-dimensionnel 

                   ALGOTEL’99-Paris

[RMM99b] S. Rivas, L. Mugwaneza, T. Muntean

Une application optimisée d’un routage adaptatif pour réseaux généraux

RENPAR-11ème rencontre francophones du Parallélisme.

[AC98]        R. Amadio, S. Coupet-Grimal

                   Analysis of a Guard Condition in Type Theory

                   1st International Conference on Foundations of Software Science and Computation

                   Structures, FoSSaCS'98s, Lisbon, LNCS 1378 Springer-Verlag

[GM98]       M. Gengler, M. Martel

                   Des étages en Concurrent-ML,Proceedings of RenPar'10, Rennes

[F98]           A. Février

                   Computer Supported Cooperative Work: TheInternet approach

                   MMACCESS98, Campinas, Brésil.

[GP98]        E.Gascard, L.Pierre

                   Two Approaches to the Formal Proof of Replicated Hardware Systems using the Boyer-

                   Moore Theorem Prover,  Proc. Int. Workshop on First Order Theorem Provers (FTP'97),

                   Linz (Austria), October 1997.

[RM98]       S. Rivas, T. Muntean

                   Une application optimale d’un algorithme de rouatge adaptatif,

                   Proc. ofRenPar’10, Rennes

[P98]           L.Pierre

                   Specification of Communicating Processes in LOTOS and in VHDL: a Case Study,

                   Proc. International Workshop on Specification Techniques and Formal Methods

                   (Invoicing'98), Nantes, March 1998.

[P97a]         L.Pierre

                   Specification of Communicating Processes in LOTOS and in VHDL: a Case Study,

                   Proc. International Workshop on Specification Techniques and Formal Methods

                   (Invoicing'98), Nantes, March 1998.

[P97b]         L.Pierre

                   VHDL Description, Boyer-Moore Specification and Formal Verification of a Parallel System

                   for Finding a Maximum,  Proc. Workshop "Formal Methods for Parallel Programming:

                   Theory and Applications", (FMPPTA'97), Geneva, April 1997.

[GM97]         M. Gengler, M. Martel

                   Self-applicable Partial Evaluation for the pi-calculus,

                   Proceedings of the 1997 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-

                   Based Program Manipulation, PEPM'97

[GG97]         C. Gavoille, M. Gengler

                   Space-Efficiency of Routing Schemes of Stretch Factor

                   Proceedings of the 4th International Colloquium on Structural Information and

                   Communication Complexity (SIROCCO97), July

[JCC97]         L. Jakubiec, S. Coupet-Grimal, P. Curzon

                   A Comparison of the Coq and HOL Proof Systems for Specifying Hardware, TPHOLs'97

[MT97]         T. Muntean, E-G. Talbi

                  Parallel Genetic Approach to solve automatic process allocation

                  Chapter in "Genetic Algorithms in Optimisation, Simulation and Modeling

                  IOS Press, Amsterdam 1997, J. Stender & al (Eds)

[M97]         T. Muntean

                  Towards Multi-Models Parallel Programming and Communications.

                  ACM Computing Survey, extrait de "Future Directions in Computing Research"

                  Workshop-ACM, MIT Press, 1997

 

 

Thèses, Habilitations

[E01]Cristian Ene

                   Un model formel pour les systèmes mobiles à diffusion

                   Thèse Université de la Méditerranée, Déc.2001

[M00] Matthieu Martel

                   Analyse Statique et Evaluation Partielle de Systèmes de Processus Mobiles

                   Thèse Université de la Méditerranée, Déc.2000

[J99] Line Jakubiec

                   Vérification de Circuits dans Coq, Thèse Université de Provence, Juillet 1999

[K99] Romain Kamdem

                   Contribution au partionnement matériel/Logiciel des systèmes temps réels pour

                     les applications de contrôle d’expérience. Thèse Université de Provence, Déc. 1999

[Pi99] Laurence Pierre

                   Contribution à la spécification et à la preuve formelle de systèmes informatiques,

                   HDR-Université de Provence, Janv. 1999

[R99]Stéphane Rivas

                   Routage adaptatif dans les réseaux généraux, Thèse Université de la Méditerranée, 1999

[A98] Christophe Aussagues,

                   Placement optimal de tâches pour systèmes parallèles temps critiques; application à un

                   système de contrôle nucléaire, , Thèse Université de la Méditerranée, 1998                    

[D97] Robert Despons

                   Conception d'une Machine Virtuelle pour les Systèmes Parallèles à Diffusion,

                    Thèse INPGrenoble

 

 

Colloques, Rapports de recherche

 

L. Klenov, L. Pierre

                   Systematic Refinement of Iterative Loops in the B Method, RR-LIM, Juin 2001

C. Ene, T. Muntean, D. Toma

                   Characterisation of Diffusing Systems, Juin 2001

C. Ene, T. Muntean

                   ∆-Calculus, a model for nomadic processes

                   RI-LIM/PARCS, Nov.1999

A. Février

                   Intenet tools for computer supported cooperative work

                    Invited talk in CSed99 Workshop at Upsalla University

J. Garmendia, S. Rivas, T. Muntean

          A generic routing model for mobile objects

          RI- LIM/PARCS, Dec.99

E. Gascard, L.Pierre

          Toward the Mechanical Verification of Distributed Programs in Symmetric Interconnection

          Networks, RR LIM/PARCS-338, Oct.99

P. Georgelin, L.Pierre, T. Nguyen

          A Formal Approach for the Specification of MPI Primitives Communications and

          Communication Mechanisms

          RR LIM/PARCS-337, Nov. 1999 Soumis à PDCS'2000

M. Martel, M. Gengler

                   Partial Evaluation of Concurrent Functional Languages, RT-354, LIM (soumis)

T. Muntean, C. Ene

          A Broadcast-based Calculus for  Communicating Systems

          RI-LIM/PARCS, Sept.1998

O. Rolland, T. Muntean

                   Refining Distributed Systems-Application to the B Method,, (soumis pour publication)


Valorisations et Collaborations

Nos travaux récents ont donné lieu à plusieurs contrats et projets de collaboration