SAFA: Sophia-Antipolis Formal Analysis Group
Detailed programs and presentation slides
Third SAFA day, INRIA Sophia-Antipolis, 2 july 2008
Slides:
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.
Page maintained by:
eric.madelaine@sophia.inria.fr