Previous | 
Home
Section: New Results
Multiple Services for Device Adaptive Platform for Scenario Recognition
Participants : Annie Ressouche, Jean-Yves Tigli.
The aim of this research axis is to federate the inherent constraints of an activity recognition platform like SUP (see section 6.19 ) with a service oriented middleware approach dealing with dynamic evolutions of system infrastructure. The Rainbow team (Nice-Sophia Antipolis University) proposes a component-based adaptive middleware (WComp [76] , [75] , [64] ) 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.
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 and 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 of synchronous models (see figure 26 ). 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. Actually, we supply a graphical interface to design both critical component behaviors and properties as observers in the synchronous language Lustre [62] . Then the validation of properties and the creation of the validated synchronous component is automatic [44] , [53] .
|
This year we focus on the main challenge of this approach which is to deal with the possibly very large number of constraints a user must specify. Indeed, each synchronous monitor has to tell how it combines with others, then we get a combinatorial number of constraints with respect to the number of synchronous monitors and inputs of the critical component. To be adaptive with efficiency, we must face this problem. We first introduced some default rules to avoid the user to express a large number of constraints. We also studied how Abstract Interpretation technique can help us to reduce this complexity. This approach works if we forbid some “non monotonic” constraints, but this is a strong limitation. Thus, it is still a challenge for us. This drawback is a popular challenge in adaptive middleware and some results exist relying on controller synthesis methods. We are not in the exact framework where these techniques apply, but we plan to study if we can rely on some extension of these techniques.
On another hand, we also want to complement our preservation result in studying how the proof of a global property can be decomposed into the proof of local ones. In general, this decomposition (known as assume-guarantee paradigm) is difficult to apply but there is no communication between synchronous monitors and so the decomposition could be tractable. Moreover, some works address this problem and we can rely on them.