The SYNCOMP project

Introduction

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 I_C as input event set. There must exist an injective mapping : in: O rarr I_C. 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.

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.

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. 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,..)

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

Use Case Implementation

• The camera has an only output warning₁, connected to the warning input of Alarm component. Its inputs are in_kitchen and close_fridge and warning₁ is emitted when both inputs are true;
• The fridge component has two outputs warning₂ and weak_alarm₂ respectively connected with warning and weak_alarm inputs of Alarm component. Its inputs are fridge_opened and one_minute . warning₂ is emitted when fridge_opened is true and one_minute is false and weak_alarm₂ is emitted when both are true;
• The posture has two outputs warning₃ and weak_alarm₃ respectively connected with warning and weak_alarm inputs of Alarm component. It listen to sitting , standing and lying and a warning₃ is sent when sitting or standing is true while a weak_alarm₃ is sent when lying .

node camera(in_kitchen,close_fridge:bool) returns(warning1:bool)
let warning1= in_kitchen and close_fridge;
tel
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;
tel
node  posture(sitting, standing,lying:bool)
     returns(warning3,weak_alarm3:bool)
let  warning3= (standing or sitting) and not lying;
     weak_alarm3 = not standing and not sitting and lying;
tel

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 warning₁, warning₂ and warning₃ are connected to the warning input of Alarm component. On the other hand, weak_alarm₂ and weak_alarm₃ are connected to the weak_alarm component. The constraint function (&zeta) must says how these respective set of events are combined:

• &zeta(warning_k) = warning (for k = 1,2,3);
• &zeta(weak_alarm₂) = weak_alarm;
• &zeta(weak_alarm₃) = weak_alarm;
• &zeta(weak_alarm₂, weak_alarm₃) = strong_alarm.

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

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;
tel

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;

tel

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:

Documentation

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