Title: Component-based Construction of Heterogeneous Real-time Systems in BIP
Speaker: Joseph Sifakis
　　　　 CNRS/Verimag/INRIA Schneider Chair
Time: 3：30pm, Tuesday Oct. 27th
Venue: Lecture room, State Key Lab of Computer Science, Level 3 Building #5,
　　　　 Institute of Software, CAS
ABSTRACT:

We present a framework for the component-based construction of real-time systems. The framework is based on the BIP (Behaviour, Interaction, Priority semantic model, characterized by a layered representation of components. Compound components are obtained as the composition of atomic components specified by their behaviour and interface, by using connectors and dynamic priorities. Connectors describe structured interactions between atomic components, in terms of two basic protocols: rendezvous and broadcast. Dynamic priorities are used to select amongst possible interactions - in particular, to express scheduling policies.

The BIP framework has been implemented in a language and a toolset. The BIP language offers primitives and constructs for modelling and composing atomic components described as state machines, extended with data and functions in C. The BIP toolset includes an editor and a compiler for generating from BIP programs, C++ code executable on a dedicated platform. It also allows simulation and verification of BIP programs by using model checking techniques.

BIP supports a model-based design methodology involving three steps:

• The construction of a system model from a set of atomic components composed by progressively adding interactions and priorities;
• The application of incremental verification techniques. These techniques use the fact that the designed system model can be obtained by successive application of property-preserving transformations in a three-dimensional space: Behavior×Interaction×Priority.
• The generation of correct-by-construction distributed implementations from the designed model. This is achieved by source-to-source transformations which preserve global state semantics.

We present the basic theoretical results about BIP including modelling interactions by using connectors, modelling priorities, incremental verification and expressiveness. We also present examples illustrating the methodology as well as experimental results obtained by using the BIP toolset.

Further information is available at: http://www-verimag.imag.fr/~async/bip.php