Specification and Generation of Safe Distributed Components
The Oasis team is working on
- the generation of finite, parameterized, models from analysis of Proactive
source code. This allows us to verify temporal properties of distributed
applications. Those properties are essentially about messages exchanged between
active objects (requests and replies), including to some extend the identity of
objetcs (but not their location) and the data values carried by the messages.
- the specification of the behaviours of active objects, in terms of
(parameterized) networks of communicating automatas. Based on the same semantic
foundations than the model we generate form code, the specifications are
expressed in a graphical manner, suitable for use by non specialists.
Logical properties of the system can be checked directly on the specification
using model-checking tools. Then the specification pieces can (in principle)
be compared with the models generated from the code of an implementation.
We are curently extending this works in the context of the ProActice/Fractal framework for
distributed (hierarchical) components. In addition to having an activity (a behaviour), a
ProActive component has non-fonctionnal features, including life-cycle (start/
stop), reconfiguration (dynamic replacement and rebinding), etc.
Policies express conditions for the management of the components
lifecycle. We are developing methods and tools for specification and verification
of safe componant-based applications, expressing the interplay of their
functional and non-functional behaviour, and their possible dynamic
reconfigurations.
Subject of the proposed thesis :
Having a common model for the specification of the application or component,
and for the behavioural semantic model is the basis of a sound principle
for model generation. Conversely, we will use this model to generate
parts of the implementation of
components directly from the specification, in a way that will guarantee
correctness properties w.r.t. the specification.
Typically, (java) interfaces can be derived automatically from the components
ADL that will express the static aspects of the composite components structure
and bindings. Then the behavioural specification can be automatically
implemented be code generation in a way that ensures correctness versus the
component specification, and ultimately correctness of components composition.
Alternatively, assertions can be generated that will check at runtime the
correctness of a developper implementation code.
Prerequisites :
- Java and/or Distributed Programming
- Programming Languages Semantics
Advisors :
Eric MADELAINE
Phone : 04 92 38 78 07 Email : Eric.Madelaine@sophia.inria.fr
Denis Caromel
Phone : 04 92 38 76 31 Email : Denis.Caromel@sophia.inria.fr
Lab : OASIS : INRIA Sophia Antipolis