Seminar details

Abstract: PhD students present their work.
- 14:00 Dellabani Mahieddine: Implementation of Distributed Real-Time applications.
Abstract: The design and implementation of distributed real-time systems is acknowledged to be a very difficult task. A central question being how to efficiently coordinate parallel activities by means of point-to-point communication so as to keep global consistency while meeting timing constraints. Considering real-time constraints brings additional complexity since any scheduling or control decision may not only impact system performance, but may also affect the satisfaction of timing constraints. In this thesis, we present a model-based and component-based approach to design distributed real-time embedded systems. Our aim is to automatically generate correct-by-construction implementations, that is, faithful with respect to their high-level representations, thus enabling us to close the gap between models used in system verification and their actual implementations.

- 14:40 Cristina Serban: Complete Proof Systems for Inductively Defined Predicates.
Abstract: We consider an induction-based approach for reasoning about entailment in the setting of separation logic with inductively defined predicates. An inductive predicate system is a finite set of rules that define predicates, where the definition of each predicate may depend on itself (i.e. be recursive) or other inductive predicates. By proving entailments involving such predicates, we want to show possible relations among them. More precisely, in the context of separation logic, we would want, for instance, to show that two different predicates describe the same state of the heap. Our approach is to build inductive proofs, by means of a generalized proof system that contains induction as a rule and that can be adapted to different types of logic (e.g. first-order logic, separation logic). We intend to characterize the logic fragment for which our proof system is complete, as we know that there are contexts which assure completeness (e.g. language inclusion for finite automata).

- 15:20 Anaïs Durand: Self-stabilizing distributed algorithm for local resource allocation.
Abstract :
Nowadays, there is a growing interest for distributed systems. For
example, wireless sensor networks are used in home automation,
earthquake monitoring, or military applications. Peer-to-peer systems
are used to share files or communicate. Due to their scale or use, it
is difficult to envision human maintenance of distributed systems in
case of faults. Fault-tolerance is therefore an important requirement
for distributed systems. Self-stabilization is a versatile technique
to withstand any transient fault in a distributed system since a
self-stabilizing algorithm is able to recover a correct behavior after
the occurrence of transient faults.
I will present an insight of my work on distributed algorithms and on
self-stabilization and then focus on a particular study about resource
allocation problems. Resource allocation consists in managing fair
access of a large number of processes to a small number of reusable
resources. As soon as the number of available resources is greater
than one, efficiency in concurrent accesses becomes an important
issue, as a crucial goal is to maximize the utilization rate of
resources. In particular, I will explain how we tackle concurrency in
the presented solution.