Our efforts
aim at developping component models endowed with a typing framework for the
safe and meaningful composition of components. The basis of our approach
relies on proving two properties for well typed configurations of components:
(i) well-typedness is maintained throughout the computations (subject
reduction) and (ii) well typed configurations yield well “behaved”
configurations. In this setting, there are different dimensions that we need
to tackle: what computational model to consider for our components, what is
the associated typing language, how expressive this typing language is, the
decidability of the typing system, and what behavioural properties can be
guaranteed. We investigate these different dimensions, exploring the
expressiveness of both the computational model and the typing language, and
working out the properties that are guaranteed. Our computational model is
based on extensions and variants of the p-calculus.
For the typing system, we follow and amplify Milner’s “sorted ports” and
Nierstrasz’s “regular types for active objects” which set the stage for
what is now termed by the “behavioural typing” approach. Indeed, in
contrast with the functional paradigm where the theory of types originated,
processes and objects do exhibit state, interaction, and behaviour. The
actions that may be engaged by a process (we can similarly talk about the
methods that may be invoked on an object) depend on its state. Using object
terminology, objects are said to manifest non-uniform service offers. Thus the
typing language should encompass information about state and behaviour.
Our first
results, developed on an extension of the p-calculus,
feature, a collection of “interface typing languages”, differing by
their expressive power, each coupled with the appropriate typing discipline,
and the guarantied behavioural properties (ranging from safety to liveness).
The typing disciplines constrain the calculus in a natural way, distinguishing
between two kinds of ports: private and sharable, and between two possible
roles played by processes for a port: client and server. More recently, we are
concerned with extending the behavioural typing results to components with
timed behaviour. We consider a contract oriented type language:
it allows for the specification of required and provided QoS features
that need to be fulfilled by the communicating components and by their
underlying infrastructure. A contract is a written document that engages
peered communicating endpoints. The timed behaviours specified in a contract
are written in a formalism close to Alur and Dill's timed automata. We show
that deciding whether peered endpoints are well-behaved regarding each other (so
that they do not lose any message) is statically decidable. We also propose a
method to verify that computational configurations possess the same property.
Our results yield a compositional method for the verification of QoS-aware
object-based distributed programs.
Our research
is now focusing on more general composition patterns, beyond client servers
and private protocol sessions. Indeed, a coordination pattern (possibly
described in an appropriate UML model) is a basis for our new interface typing
language. Multi-party, general purpose contracts can be formally defined and
verified allowing for the safe and meaningful composition in a rich
coordination environment. A typical application domain is feature and service
composition.
Elie Najm
Professeur - ENST
Dépt. Informatique et Réseaux
46, rue Barrault
75634 Paris Cedex 13
France
Elie.Najm@ENST.fr
Voice: + 33 (0)1 45 81 77 09
Fax: + 33 (0)1 45 81 31 19
Academic partner of Esterel EDA Technologies
provider of ESL synthesis
for control-intensive IP,
including formal verification of assertions, SystemC,
VHDL, and Verilog code generation
Academic partner of Esterel Technologies, the provider of model-based solutions for
DO-178B and IEC 61508 safety-critical systems.
