Associated team D.S.T : Activity report 2010

This page summarizes the work accomplished since the last activity report in October 2009.

1. Scientific results

Quasi static scheduling

The main objective in quasi static scheduling (QSS) is to synthesize a global scheduler for a distributed system composed of communicating processes. This scheduler can only impose which process has the right to perform the next action, but can not decide which action the selected process should play. The objective of the scheduler is to avoid bad properties of the system (deadlocks, violation of safety rules,...) just by enabling/disabling processes. A solution to this problem was published in 2009, to ensure that the communication buffers of the system remain within a certain bound without blocking the system. More interesting properties can also be granted by scheduling.
We are now addressing a distributed version of this problem, by relaxing the global scheduler hypothesis. Each process is controlled by a local supervisor, that can decide whether its observed process has the right to perform an action or not. This problem is much more complex than centralized QSS, as the existence of a global scheduler does not guarantee the existence of local ones. We have progressed this work during the visit of S. Paul (IMSC) in november 2009, but so far obtained no satisfactory solution.

Realistic implementation

A lot of work has been devoted to translation from High-level specifications to distributed machine models. Such work exists for to translate automata into communicating finite state machines (CFSMs), scenarios (HMSCs) into CFSMs, etc. However a translation is considered correct if and only if it synthesizes a machine model with an equivalent language. When CFSMs are used as target model, the machine model can contain deadlocked runs. The language of CFSMs only considers runs that reach final states (usually configurations in which all automata are in their final states and with empty communication buffers), but rules out deadlocked runs, that might nevertheless appear if a protocol is implemented as described in the communicating machines, and all prefixes of runs.
Even if this setting is correct with respect to distribution and language equivalence, the semantics of the obtained CFSMs is not that of a real implementation.
We consider different settings :

Consider the language of a CFSM as the prefix closure of all runs (including deadlocked ones) : this means in particular that one can not rule out deadlocked behaviors to preserve language equivalence between a specification and its implementation. This situation is closer to real-life protocols: an interaction that end with a deadlock is still a behavior of the implementation. R. Abdallah is currently extending synthesis algorithms from Scenarios and implementing them in the SOFAT toolbox. The objective is to extend this prototype to obtain a demonstrator for realistic implementation techniques.

Consider language equivalence up to some projection, that is allow for additional synchronization messages among communicating machines to realize a specification. An initial solution was proposed by B. Genest. In his solution, a copy of the original specification is kept in the system, and all machines synchronize to chose the next action to perform. The challenge is now to synthesize the minimal implementation, with respect to the synchronizations, messages exchanged, or memory used by each machine to realize a global specification. Some work has been initiatedwith Madhavan Mukund and Narayan K. Kumar from CMI in this domain.

Quantitative analysis of time

We have initiated some work on fluid event graphs. In this model, transitions fire according to a constant firing rate (thus the number of token in each place may not be integer). In the case of live and bounded event graphs, one can compute the exact behavior of the system, and even give some properties about the "speed" of the system for the transient phase. This can be extended to systems with inputs/outputs to allow some modularity due to the compositionnality of those systems (concatenation, synchronization and feed-back control). Extensions of this work will include the study of this kind of system when the firing rates are not fixed but lay in an interval and multi-mode analysis: there the firing rate changes according to some actions that can be described by a simple timed automaton.

Another study concerns the analysis of timed systems crossed by flows that are completely ordered by priorities. This study has been made during Aurore Junier's master thesis. We have exhibited an algorithmically and numerically efficient method to compute worst-case delay upper bounds using the Network Calculus framework. Our algorithms improve the existing bounds and are a mixing of purely (min,plus) techniques and linear programming. An article will be submitted at Valuetools 2011 to present these results.

Modeling of Worklfows and Web Systems

Web service architectures are usually described through session centric formalisms, such as BPEL, workflows formalisms such as ORC, or site per site formalism (as for instance in AXML). Whenever a formalism is chosen, it lacks the characteristics of all others: BPEL is not tailored for orchestrations, ORC misses the notion of correlation which is essential to establish sessions among participants to a service. Site per site formalisms lack a clear presentation of workflows, which are useful to reason on causal dependencies between sub-services that compose an orchestration.

During the visit of Madhavan Mukund in Rennes in May 2010, we have proposed a formalism inspired from these three worlds, that compose sessions. We voluntarily restricted the expressiveness of the language in such a way that verification of simple properties become feasible. The result can be described as sets of processes that can create asynchronously an arbitrary number of sessions (finite behaviors), or participate in existing sessions, playing different roles in each one. At this point of our study, it seems that the semantics of this formalism is captured by well-structured transition systems, which would allow for the decidability of several interesting properties. We expect a common publication on this topic next year.

Verification of timed MSCs

Verification of Message Sequence Charts is an undecidable problem in general. However, reasonable subclasses, such as globally cooperative MSCs have been identified, and allow for the decidability of some verification problems. A recent extension of scenarions, called time-constrained MSCs extend scenarios with time. This formalism allows to define time constraints as time intervals between occurrence dates of events. The introduction of these light annotations brings a lot of undecidability in HMSCs. It is even undecidable whether an annotated HMSC allows for a single timed execution matching all the constraints (this is called the emptiness probem) ! The only case when this problem is decidable is when the considered HMSC defines a regular language. To deal with this situation, and go beyond bounded (regular) MSCs we want to find some syntactic restrictions that still allow for unbounded behaviors while preserving some decidability.

During the December 2009 visit of Distribcom members to NUS, we have redefined the semantics of time-constrained MSCs as behaviors of some kind of hybrid automaton. This does not bring decidability, as emptiness in hybrid automata is undecidable in general. However, upon several assumptions, we think that we can bring back the emptiness problem to the study of a regular set of representants of all behaviors of the system. These assumptions are the following:

- local clocks of processes do not drift too far away from one another

- only a bounded number of events can occur in a bounded time interval (this property is close to non-zenoness in timed automata)
- all processes have a real-time behavior, that is the occurrence dates of the n-th event on a process is k*d + e, where d is the rate of the process clock, k>n is some integer, and e is a small positive or negative value modeling clock jitter.

We think that these assumptions are sufficient to ensure decidability of emptiness, and we plan to progress this work in december 2010 to obtain some publishable results.

2. Exchanges 2009/2010

no	name	Senior/Junior	dates	origin	Destination	Funded by	Cost	Note
1	Soumya Paul	J	13-17 /12 /2009	Chennai(IMSC)	Rennes	DST 2009	818
2	Blaise Genest	S	27/11/2009 - 14/12/2009	Rennes	Singapore	DST 2009	3198,86
3	Loïc Hélouët	S	28/11/2009 - 7/12/2009	Rennes	Singapore	DST 2009	2847,93
4	Anne Bouillard	S	05-15 /02/2010	Rennes	Singapore	DST 2009	2772,88
5	Blaise Genest	S	23-27/02/2009	Singapore	Chennai	ANR DOCFLOW	1335,48
6	Loïc Hélouët	S	30/01 - 04/02/2010	Rennes	Chennai	ARCUS (region Ille de France)	1162,96
7	Madhavan Mukund	S	04-08/05/2010	Chennai via Bordeaux	Rennes	DST 2010 + ARCUS	689,46
8	Claude Jard	S	21-26/09/2010	Rennes	Singapore	DST 2010	2500	Estimated cost
9	Albert Benveniste	S	20-26/09/2010	Rennes	Singapore	DST 2010	2500	Estimated cost
10	Loïc Hélouët	S	02-10/12/2010	Rennes	Singapore	DST 2010	3000	planned - estimated cost

3. Financial report

3.1 Funded by DST (2009 and 2010)

Expenses	Amount (DTS 2009)	Amount (DTS 2010)	TOTAL	Note
Invitation of partners	818	689,46	1507,46
INRIA missions	8819,67	8000,00	16819,67	Estimated
TOTAL	9637,67	8689,46	18327,13

3.2 Funded by external support

Expenses	Amount (Oct. 2009 -> Dec 2010)	Note
Invitation of partners	--	The flight from Chennai to Paris was financed by ARCUS for mission 7
INRIA missions	2498,44	Missions 5 & 6 were financed by ANR Docflow and ARCUS A part of the travel for mission 9 was financed by external funds.
TOTAL	2498,44

Total funds used : 20825,57

4. Program for 2011

The work programme for 2011 is a followup of the activities started in 2010. Note that as Anne Bouillard left the Distribcom team, the activities around quantitative analysis of time will not be pursued within DST.

Quasi static scheduling

We plan to continue the work initiated on distributed quasi static scheduling. The people involved are: B. Genest, S. Yang, S. Paul, Ph. Darondeau, L. Hélouët.

Realistic implementation

R. Abdallah will continue working on realistic implementation of MSCs, and integrate her results in our prototype SOFAT. Ph. Darondeau, L. Hélouët, M. Mukund and N.K. Kumar will also study realistic implementation from different models (for instance transition systems without the diamond property).

Modeling of Woklfows and Web systems

We will continue the work started in 2010. We have defined a session composition model. This is a preliminary work, and the model might need some cleaning. We can also focus on the properties of the system. Reachability, schedulability, .... A first step is to show that our conjecture that our model defines well structured transition systems holds. We expect a common publication on this topic this year.

Verification of timed MSCs

We plan to use the hybrid automata semantics for time constrained MSC in 2009, and region construction techniques to solve the emptiness problem. When a solution is found, decision techniques for more elaborated questions might follow, but this first step is essential. We will define the needed syntactic restrictions on TC-MSC and on the targetted architecture so that region construction becomes feasible.

5. Exchanges

We have planned 7 travels in 2011, and we will hire an intern from may to july 2011.

5.1 From INRIA to Partner

	nb	Cost EA	External Funding	Total
Senior researcher	3	5500	3000	8500
PhD	1	2500		2500
Total	4	8000	3000	11000

5.2 From Partner to INRIA

	nb	Cost EA	External Funding	Total
Senior Researcher	1		3000	3000
PhD	1	2000		1500
Internship	1		2800	2800
Total	3	2000	5800	7300

5.3 Estimated Costs for the team and funds required

	Amount
Gloabal cost of year 2011	18800
External funding	8800
Required funding	10000

5.4 Schedule of exchanges (Temptative)

The table below is only a temptative schedule for planned exchanges, and is built from the composition of teams in 2010, and from former exchanges that took place in 2009 and 2010. There might be significant changes in the final shedule, name of person involved, but not in the number of missions planned nor on the covered topics.

Person involved	Destination	Possible Date	Topic
Loic Hélouët	Chennai	February 2011	Workflow Modeling
Loïc Hélouët	Singapore	November 2011	Timed MSCs - Quasi static Scheduling
Philippe Darondeau	Chennai	October 2011	Realistic Implementation
Rouwaida Abdallah	Chennai	October 2011	Realistic Implementation
Madhavan Mukund	Rennes	May 2011	Workflow Modeling
Phd Student (Chennai)	Rennes	to be defined	Workflow Modeling or QSS

6. Funding

In addition to the INRIA support for our associated team, we can expect some support from the following sources:

P.S.Thiagarajan has a 30000S$ (approx 15 000 euros) support from NUS for all the duration of the collaboration.

Both S4 and Distribcom are involved in DISC: Distributed Supervisory Control of Large Plants, an european project of the 7^th PCRD that might provide additional financial support for the team, in the supervisory and control theme. DISC will provide 40.6 k Euros to IRISA in 2011.

Distribcom is involved in DOTS: Distributed, Open and Timed systems, an ANR Security Project. This project has been extended until december 2011. It might provide additional financial support for the team, in the timed and games aspect of the theme. DOTS will provide 8.8 k Euros to DISTRIBCOM in 2011.

Last year, a mission to chennai was supported by the ARCUS project ( a project of Region Ille-de-France for french/indian collaboration), at the occasion of the ACTS conference in Chennai. It is possible that this will also occur in 2011 (note however that we did not include it in our cost estimation, as this funding is not guaranteed)

The research started this year on workflows modeling is close to the topics of project ACTIVDOC funded by region Bretagne. We plan to use it to finance an internship and an invitation of one of our indian partners. The ACTIVDOC project will provide 47.5 k euros to Distribcom in 2011.