Associated team D.S.T  :  Research Themes


This associated team is a tripartite collaboration between two projects at INRIA Rennes (S4 & Distribcom), the National University of Singapore (NUS), and two institutes in Chennai (INDIA), the Chennai Mathematical Institute (CMI) and the Institute of Mathematical Sciences (IMS). The objective of the DST project is to study distributed systems, supervision and time issues with the help of concurrency models. The two main themes of the project are supervision, and quantitative/timed aspects of systems. The supervision theme will focus on distributed scheduling policies of distributed systems to ensure satisfaction of some properties (preservation of some bound on communication channels, for instance), diagnosis, and distributed control techniques. The second theme on time aspects of distributed systems will focus on the analysis of qualitative and quantitative properties of timed systems and models. The quantitative approaches will rely on network calculus applied to multimode Real Time Calculus, and the timed models studied during the collaboration will be inspired from timed scenarios. We expect some interactions between the two themes, that is improve timed characteristics (throughput, …) using supervision techniques, or conversely use some knowledge of time in a system to perform more accurate diagnosis and supervision.

 Theme 1 : Supervision and Control

We want to address two main themes: the first one is supervisory control, i.e. calculus of a controller or a set of controllers supervising a system, so that the monitored system satisfies some given properties. The second one is scheduling, that is finding adequate order for the activation of autonomous component such that some objectives are always fulfilled.

Theme 2 : Time

 The second theme addressed by the DST project is time in distributed systems. We want to address time from three points of view. The first one is the study of quantitative aspects, using techniques such as (Max,+) algebra, and the network calculus, for which both Distribcom and NUS have strong competences. The second aspect is the modelling power of timed model: several members of Distribcom and of CMI are very involved in research around Message Sequence Charts, a true concurrency model based on composition of partial orders. This model has been extended with time recently, and raises new challenges. The third aspect is the use of time as additional information for supervision.

·        Quantitative aspects : an important aspect in the analysis of systems is the study of the worst-case bounds for their performances. Some performance oriented models such as Network Calculus have already been proposed for static analysis. Within this setting, a system is seen as interconnected servers that treat incoming requests according to a service policy. However, with this model, the parameters of a system never change: arrival and service policies of servers do not evolve with time. Some models where these parameters can change have been proposed, such as event count automata and multimode Real time calculus. Event-count automata count the number of events that can happen at each time. In each state, the number of events is lower and upper bounded. Transitions are conditioned to some guards on counters, and when a transition is fired, some counters can be reset. These models are equivalent to timed-automata, and hence their analysis can lead to state-space explosion. During the CASDS collaboration, we have studied an intermediate model called the "multimode Real Time Calculus": arrival processes obey to some Network Calculus constraints, but these constraints can change from time to time. This is modeled by two finite automata (an arrival automaton and a service automaton), whose states can change with transitions between states caused by different signals. In the arrival automaton, an arrival curve is associated to each state, as well as a time interval where the state can change. Moreover, transitions can be guarded by some predicates depending on the parameters of the systems (fill-level for example). The service automaton is defined similarly, with service functions. We have first tried to find some efficient ways of analysing these multimode systems. Two models can be efficiently analysed: when the arrival and service automata are synchronous (the automata change their state exactly at the same time) and when they are totally asynchronous (one can find an equivalent arrival curve and an equivalent service curve). We plan to continue the work on this kind of model, and extend the analysis to cases where automata are not purely synchronous or purely asynchronous, but rather a mix of both models. The solution to find efficient analysis techniques could be to mix the two approaches used in the synchronous and asynchronous cases. 


·        Timed concurrent models and their properties: We propose to study properties of timed concurrent models, and more precisely of timed scenarios. A recent extension that adds time constraints to Message Sequence Charts (MSCs) have been proposed [AMN07]. This new model also brings several new challenges. For instance, checking time constraints on timed MSCs is an undecidable problem in general, and a solution have been proposed for the class of regular MSC languages. An interesting challenge is to study if timed constraints checking applies to other MSCs outside this class. The difficulty is to find a way to verify these constraints over a regular set of representants. However, in the general case, unbounded MSCs with generic constraints can be used to encode two counter machines, leading to undecidability. Another question is whether the timing constraints imposed on an MSC make executions channel-bounded. In general, this question is also undecidable, but there could be a solution for a restricted class of constraints. Note that timed scenarios are seen as a starting point, but that several other true concurrency models might be studied, such as communicating automata, traces….


·        Channels with losses : nowadays, MSCs only describe messages that are lost + found, or necessarily received. However, in realistic communication protocols, messages that arrive too late can also be declared obsolete. According to the MSC terminology, such messages are received. An interesting question is then to consider messages that are sent, and forgotten if not received in time. This model also differs from models with lossy channels, as losses here do not depend on a probability, but rather on time thresholds. Such model has never been proposed, but we have the intuition that this extension could be done using the extended MSCs of Martin Leucker [Leucker02].


·        Timed diagnosis : So far, very few work address diagnosis with time [Chatain06]. By diagnosis, we mean the following problem. A distributed system is equipped by sensors (either material part or code instrumentation) that send some observations to a supervisor. These observations are collected to form a partial view of an execution of the system. The question addressed by diagnosis is, from a given observation O of the system and a model M, find every explanation of the observation compatible with O. Several approaches have been proposed, using automata or Petri nets as models. Thomas Chatain has proposed a technique based on Timed Petri nets unfoldings. In a recent work, we have proposed an untimed scenario-based approach [HGG06]. The interest of this approach is to compute a finite representation of all possible explanations for an observation under the form of a High-level MSC. An interesting extension to this work would be now to consider diagnosis from scenarios with time, that is use the information on the execution dates of some events in the observation and the time constraints in the scenario model to refine diagnosis.


In addition to these two main themes, we expect some cross-theme works. For instance, we are interested in supervision techniques that would allow to maintain a given quality of service. Using quantitative information on the model may also be useful to get more efficient algorithms for control and to have a more accurate view of the behaviors of the systems.

Research Themes Team Members Publications History Miscellaneous

Copyright 2010 © DST associated team