ACI Alidecs
Réunion de travail
Paris, LIP6

lundi 12 mars 2007

Salle 549, 104, AV. du Président Kennedy, 75016 Paris
(Métro Passy, Bus 70, 72, RER C : AV. du Président Kennedy).
Prévoir une pièce d'identité.

Programme (pdf)

10h - 10h45: Frédéric Boussinot "Le language FunLoft".
FunLoft permet une programmation concurrente sûre à base de threads. Plus précisément, des contrôles statiques (système de types et effets) assurent l'absence de data-races et la finitude de la mémoire utilisée. Les threads sont liés à des schedulers, implémentés par des threads natifs, qui les exécutent de manière coopérative. FunLoft permet, en découpant une application en plusieurs schedulers, de bénéficier des architectures multi-cores. On illustrera ce point avec un exemple de simulation : le jeu de la vie.
11h - 11h45: Louis Mandel "Réactivité en ReactiveML"
ReactiveML est une extension de OCaml basée sur le modèle réactif synchrone. Dans ce modèle, l'ordonnancement est coopératif. Ainsi, pour garantir la réactivité du système, il faut vérifier que tous les processus coopèrent. Dans cet exposé, nous présenterons une première analyse statique permettant de distinguer les expressions qui s'exécutent en un instant des expressions qui s'exécutent en plusieurs instants. Nous présenterons ensuite une analyse permettant de détecter les boucles instantanées.
12h - 12h30: Florence Plateau "Horloges abstraites pour le N-synchrone".
14h - 14h45: Florence Maraninchi MWCEC : Modular Worst-Case-Energy-Consumed
We will study a component-based framework for models of non-functional properties, with the following ideas:
- Each component has a non-functional model in the form of an automaton (a discrete control structure) that transforms a sequence of external functional inputs into a value for the non-functional quantity.
- There are composition operators for such models, in particular a parallel composition, to express the many ways in which components can be assembled.
- There exists an order between two such models, $M_1 \leq M_2$ meaning that and are models for the same system, but is more precise than . Typically, if the non-functional quantity is expressed as worst-case values, a more precise model is a model in which the worst-case values are smaller.
- There is a global property to guarantee that the order is preserved by compositions: replacing a component in a global model by a more precise version should yield a new global model which is indeed more precise than . This abstraction preservation property is essential when playing with various abstractions of the individual components.
15h - 15h45: Bachir Djafri "La vérification formelle de propriétés de systèmesà base d'agents (code) mobiles".
Cette présentation illustre le passage d'une description d'architecture de systèmes à base d'agents mobiles vers un prototype d'application respectant diverses propriétés. Nous nous focalisons dans cette présentation sur la partie comportementale des agents mobiles que nous exprimons en termes d'une algèbre de processus adaptée à la mobilité (KLAIM). Cette description donne accès à des sémantiques cibles (réseau de Petri) analysables automatiquement par des techniques de model-checking ou de simulation."
15h45 - 17h: Discussion