INRIA Sophia Antipolis-Méditerranée
2004 route des lucioles
BP93 06902 Sophia Antipolis France

The SYNCOMP project


The aim of the SynComp project is to federate the inherent constraints of an activity recognition platform like SUP (Scene Understanding Platform ) designed in Stars team with a service oriented middleware approach dealing with dynamic evolutions of system infrastructure. The Rainbow team proposes a component-based adaptive middleware WComp to dynamically adapt and recompose assemblies of components. These operations must obey the "usage contract" of components. The existing approaches don't really ensure that this usage contract is not violated during application design. Only a formal analysis of the component behavior models associated with a well sound modeling of composition operation may guarantee the respect of the usage contract.

Proposed Approach

The approach we adopted introduces in a main assembly, a synchronous component for each sub assembly connected with a critical component. This additional component implements a behavioral model of the critical component. Indeed critical components will provide a synchronous model of their behavior and some additional properties (constraints) checked when component is used. This model is designed as a Mealy Machine where each output is connected with an input event of the critical component. Let us consider a synchronous monitor specified as the Mealy machine M with O as output event set and connected to a critical component with IC as input event set. There must exist an injective mapping : in: O rarr IC. In such a setting, model checking techniques apply to verify safety properties concerning this critical component. Thus, we consider that the critical component is validated.


An example of synchronous monitor managing the access to the critical alarm proxy component from a posture sensor assembly

When a critical component has multiple synchronous monitors corresponding to several concern managements in the application, we want to build an only synchronous model component which agrees with all these primitive synchronous monitors . To specify how output events sent by different synchronous monitors and connected to a critical component, we introduce a sound (with respect to our mathematical formalism) operation of composition under constraints (&otimes|&zeta) of synchronous models . This operation rely on the synchronous product of mealy machines on which we apply a constraint function (&zeta).

We proved that this operation preserves already separately verified properties of synchronous components. This operation is an answer to the multiple access to critical components.

Example of multiple access to alarm critical component; left : the synchronous monitors introduced from camera, fridge and posture assemblies, right: the composition under constraints operation.

Practical Issue

WComp middleware

We apply these results in the framework or our experimental middleware WComp.

  • WComp is a middleware for ubiquitous and ambient computing;
  • It is based on services for devices software infrastructure (relying on UPnP protocol);
  • It manages interactions between devices at runtime using a component-based architecture and event flows.

WComp Synchronous Monitor Design

To encode synchronous components we rely on the Lustre synchronous language . It is a data flow language offering two main advantages:

  1. It is a functional language with no complex side effects. This makes it well adapted to formal verification and safe program transformation, since functional relations over data flows may be seen as time invariant properties. Also, reuse is made easier, which is an interesting feature for reliable programming concerns;
  2. )
  3. Its equational nature offers us straightaway representation of both Boolean equations and non Boolean equations related to physical constraints. Thus, the call to an external constraint solver is avoided.

We choose this language because, first, Mealy machines are models for it and its compilation provides an implicit representation of them. Second, the synchronous product we rely on to perform the composition of synchronous monitors is expressed naturally in the language. Third, constraint functions can be expressed as equations, thanks to the equational nature of the language.

To perform safety properties validation we rely on the model-checking tool Lesar , a symbolic, BDD-based model-checker for Lustre. It is based on the use of synchronous observers , to describe both the properties to be checked and the assumptions on the program environment under which these properties are intended to hold. An observer of a safety property is a program, taking as inputs the inputs/outputs of the program under verification, and deciding (e.g., by emitting an alarm signal) at each instant whether the property is violated. Running in parallel with the program, an observer of the desired property, and an observer of the assumption made about the environment one has just to check that either the alarm signal is never emitted (property satisfied) or the alarm signal is emitted (assumption violated), which can be done by a simple traversal of the reachable states of the compound program. Hence, using observer technique allows to express the property in the same language used to design our synchronous components and avoid to express &forall CTL* formulas.


Verification with Lesar is performed on an abstract (finite) model of the program. Concretely, for purely logical monitors the proof is complete, whereas in general (in particular when numerical values are involved) the proof can be only partial. In our approach, component events are associated with two Lustre variables, a Boolean variable is related to the presence of the event, the other carries it's value. Thus, properties related to presence or absence of events can be proved, but properties related to values depend on the abstraction performed by the tool.

Use Case

Use Case Despcrition

To illustrate our method, we will consider the design of a small part of an application in the domain of health care for elderly.The purpose is to monitor old people in an instrumented home ( with cameras, contact sensors, accelerometers,..)

Gerhome house.jpg

the instrumented home has 4 sensors: a camera to locate the person , a contact sensor to determine the state of the fridge door (opened or closed), a timer to know how long the fridge door is opened, and accelerometers to determine if the person is standing, sitting or lying.

We consider the recognition of activities related to kitchen usage. The goal is to send several kinds of alarms depending on sensor observation results. Component proxies are associated these four sensors.

Use Case Design

In this application, an Alarm component proxy receives three kinds of alarms: warning, weak_alarm and strong_alarm. It is linked with assemblies of components for fridge and timer sensors, camera sensor and posture sensor. This Alarm component is critical and we will ensure that it raises the appropriate alarm in the designed application. To this aim, we offer a mean to ensure that each output event coming from one of the assemblies for sensors is correctly sent. In this use case, there are three sub-assemblies linked to the critical Alarm component. Thus, we introduce three synchronous monitors in this assembly. The first synchronous monitor describes the behavior of Alarm component with respect to the sub assembly managing the camera device; the second is defined with respect to the sub assembly related to the door fridge ; and the third tells the behavior of Alarm when it is related to a sub assembly managing the posture detection sensor. The posture synchronous monitor has been already described above . Then, we get an assembly also described above and we can see that warning and weak_alarm entries have multiple access. Our method will replace these three components by a single component camera &otimes fridge &otimes posture |&zeta .

Use Case Implementation

To implement this use case, we first implement the three synchronous monitors with the Lustre language. The Alarm component has three input events, corresponding to three levels of alarms: warning, weak_alarm, strong_alarm.

node camera(in_kitchen,close_fridge:bool) returns(warning1:bool)
let warning1= in_kitchen and close_fridge;
node   fridge (fridge_opened, one_minute: bool) 
     returns (warning2, weak_alarm2: bool);
let warning2= fridge_opened and not one_minute;
    weak_alarm2= fridge_opened and one_minute;
node  posture(sitting, standing,lying:bool)
let  warning3= (standing or sitting) and not lying;
     weak_alarm3 = not standing and not sitting and lying;

We replace these three components by a single component : camera &otimes fridge &otimes posture |&zeta, as said in the previous section. This composition component is a Mealy machine, which has for input event set the union of the respective input event sets of the camera , fridge and posture , ie {close_fridge, in_kitchen, fridge_opened, one_minute, standing, sitting, lying }. The output set of the composite component is O= { warning, weak_alarm, strong_alarm} and there is an obvious bijectiob between O and the input set of the Alarm component.

Looking at the definition of camera, fridge and posture synchronous components, we can see that on one hand warning1, warning2 and warning3 are connected to the warning input of Alarm component. On the other hand, weak_alarm2 and weak_alarm3 are connected to the weak_alarm component. The constraint function (&zeta) must says how these respective set of events are combined:

For all other outputs of synchronous components, &zeta respects the initial connection (since there is no multiple acces to an input of Alarm component).

Then, we implement the composition operation with respect to &zeta in Lustre:

node alarm_comp (close_fridge, fridge_opened, one_minute, standing,  
                                          sitting, lying, in_kitchen : bool)
            returns (warning, weak_alarm, strong_alarm : bool)
synchronous product 
var warning1, warning2, warning3, weak_alarm2, weak_alarm3 : bool;
let  warning1 = camera(in_kitchen, close_fridge);
    (warning2, weak_alarm2) = fridge(fridge_opened, one_minute);
    (warning3, weak_alarm3) = posture(standing, sitting, lying);
applying &zeta 
    warning = warning1 or warning2 or warning3 ;
    weak_alarm = weak_alarm2 xor weak_alarm3;
    strong_alarm = weak_alarm2 and weak_alarm3;
Now, we want to verify the alarm_comp node behavior before introducing it in the assembly. As mentioned before, we use the observer technique to prove that if the fridge is opened for more than one minute and the person is lying, then a strong alarm is sent. To this aim, we define the following verif node. It listens all the entries the alarm_comp node listens and it computes a Boolean output prop. Then the model checker Lesar verifies that prop is always true, assuming that standing, sitting and lying are exclusive.

node verif (close_fridge, fridge_opened, one_minute, standing, 
                         sitting, lying, in_kitchen : bool) returns (prop: bool)
var warning, weak_alarm, strong_alarm : bool;
let (warning, weak_alarm, strong_alarm) =  
           alarm_comp(close_fridge, fridge_opened, one_minute, 
                standing, sitting, lying, in_kitchen);

    assert (not ((standing and lying) or (standing and sitting) or 
               (lying and sitting)));

   prop = if (fridge_opened and one_minute and lying) then strong_alarm 
          else true;


On another hand, we just want to touch on the application of preservation ability our method offers. Assume that with Lesar, we prove that for fridge component, the property: fridge_opened &rArr warning2 holds. From the definition of the constraint function, we have &zeta(warning2) = warning Thus, we can deduce that fridge_opened &rArr warning also holds in alarm_comp.

After this verification, we automatically generated WComp input code for node alarm_comp. Thus this new component has been automatically weaved in the assembly designing the application in WComp:

Wcomp assembly


slides of the presentation at Software Composition conference (SC2011).

return top