SAFA: Sophia-Antipolis Formal Analysis Group
Detailed programs and presentation slides

SAFA workshop, INRIA Sophia-Antipolis, december 3, 2008
Batiment Kahn, Amphi Morgenstein

Third SAFA day, INRIA Sophia-Antipolis, 2 july 2008

• Mireille Blay-Fornarino (Rainbow, I3S): Evaluation based composition of activity model
• Sophie Coudert (Labsoc, Telecom-ParisTech) : Prouver en B une propriété de sécurité d'un système basé sur un micronoyau.
• Marcela Rivera (Oasis, INRIA) : Stopping Safely Hierarchical Distributed Components: Application to GCM

Details:

• Mireille Blay-Fornarino (Rainbow, I3S): Evaluation based composition of activity model
  Separation of concerns, step-wise development and application adaptations require development and execution tools to support application composition. Depending on the domain, the composition mechanisms are different as well as the "expected properties" such as composition associativity, conflict detection, idempotence... We propose to consider composition of activities in a general way but adaptable to different technological domains. We model each application as a graph of activities and we are interested in the composition of these graphs by means of "merging" functions which are defined and evaluated differently according to the targeted domains. To illustrate this approach we take examples from two domains : service orchestration composition and composition of interactions between heterogeneous components. But other domains have been studied and they conform to this approach of activity composition. First, we point out through examples the requirements for implementing composition independently from domain specificities. Then we define a metamodel to design the activity flow as a graph. This metamodel has to be refined according to the targeted domain. This structure is the base for our composition algorithm which is defined in a general way by means of dependent domain functions. Finally some properties expected from activity compositions are characterized and we identify the properties that must be checked at domain level. This work comes from our experience and studies on composition of software applications. The metamodelisation and semi-formal approach allow us to have a new point of view on technological issues independently of targeted platforms. Comparisons, property verification and even developments are then easier.
• Sophie Coudert (Labsoc, Telecom-ParisTech) : Prouver en B une propriété de sécurité d'un système basé sur un micronoyau.
  Cet exposé est un compte rendu d'expérience à l'issue d'un projet au cours duquel on a expérimenté la méthode B et son outillage avec pour objectif de garantir une propriété de sécurité à propos d'un système basé sur un micronoyau. Ce cas d'application et son contexte (OS et implémentation pré-existant du micronoyau) étaient nouveaux pour B. Le principal résultat est la méthodologie de preuve finalement mise en oeuvre qui fait intervenir divers aspects de B. Ce travail a également permis de mettre en évidence d'autres exploitations possibles d'une modélisation B qui seront rapidement présentées, ainsi que quelques considérations annexes quant à l'approche micronoyau.
• Marcela Rivera (Oasis, INRIA) : Stopping Safely Hierarchical Distributed Components: Application to GCM
  We propose an algorithm for safely stopping a subsystem of a component assembly. More precisely, it safely stops a component and all its subcomponents in a distributed and hierarchical component model. Our components are distributed, autonomous, and communicate asynchronously. Thus, one of the great challenges addressed by this paper is to synchronise those components during a process which involves their deactivation. This algorithm has been prototyped and evaluated experimentally in a distributed component example. We also describe the main properties of our algorithm (both correctness and termination) and its requirements on the component system to be stopped.