Round Table 2015-12-03

  • Vincent Kherbache
    • Scheduling Live-Migrations for Fast, Adaptable and Energy Efficient Relocation Operations [slides]

28-29 Sept Active-object “workshop”

The 28 and 29 Sept the Scale team organises a small informal workshop on the current and future trends on active-objects, actor languages, and the verification tools for those languages. It will be in rooms Kahn 1 and Kahn 2. Everybody is welcome to attend and participate.

Program (preliminary)
!!! Each talk has a 45 minutes time-slot in order to leave plenty of time for discussions — Consequently, please plan on approx. 30 minutes of presentation; also please try to present your current and future works (at least in the conclusion of your talk) in order to trigger even more discussions.

12:30    lunch at inria
14:00    introduction and brief presentation of the participants
14:30    sharing objects in ponyrt —Albert Yang — slides
15:15    Deploying ABS active objects using the ProActive library — Justine Rochas and Ludovic Henrio — slides
16:00    coffee break
16:30    Modelling an open-source data center kernel in ABS — Behrooz Nobakht
17:15    State of art and challenges in deductive verification of concurrent programs with cooperative scheduling — Crystal Din — slides

9:15    A Design Pattern for Modelling Parallel and Distributed Applications using ABS and JAVA 8 — Vlad Serbanescu — slides
10:00    Coffee break
10:30    Integrated environment for verifying and running distributed components — Oleksandra Kulankhina
11:15    A workflow for statically verifying program properties — Abel Garcia
12:15    lunch at Restaurant in Sophia (Le Provencal Golf)
14:00    Deadlock analysis for concurrent and distributed programming— Vincenzo Mastandrea
14:45    Integration of active objects with parallel combinators — Kiko Fernandez
15:30     wrap up and global discussions
16:00    coffee break (and discussions)

Round Table 2015-06-29 & 2015-06-30

  • Miguel Oliva
    • Adaptable Stream Processing Using GCM (Master defense rehearsal) []
  • Mario Taddei
    • An integrated system for building and running reproducible research (Master defense rehearsal) [slides]
  • Alexandros Tsantilas
    • Analysing bugs in VM Schedulers (Master defense rehearsal) [slides]
  • Pavlo Khvorostov
    • A viewer tool for multiactive objects (Master defense rehearsal) []

Round Table 2015-03-17

  • Ph.D. Pedro Velho
    • GreenHPC: A Novel Framework to Measure Energy Consumption on HPC Applications []

Round Table 2015-03-02

  • Eric Madelaine
    • pNets: an Expressive Model for Parameterised Networks of Processes (PDP’15) []
  • Sophie Song
    • Solutions for Processing K Nearest Neighbor Joins for Massive Data on MapReduce (PDP’15) []

Soutenance de thèse de Nuno GASPAR // PhD defense on the 16th December 2014 at I3S(Algorithmes) at 1.30 pm

Title: Mechanized support for the formal specification, verification and deployment of component-based applications.
Jury composition:
Advisors:  Eric Madelaine (INRIA)
                  Ludovic Henrio (CNRS)
reviewers: Frédéric Loulergue (Université d’Orléans)
                  Alan Schmitt (INRIA)
examiners: Luis Barbosa (Universidade do Minho)      
                   Yves Bertot (INRIA)
                   Denis Caromel (Activéon)
In this thesis we address the formal specification, verification and deployment of distributed and reconfigurable GCM applications. Our first contribution is an industrial case study on the behavioural specification and verification of a reconfigurable distributed application: The HyperManager. This promotes the use of formal methods in an industrial context, but also puts in evidence the necessity for alternative and/or complementary approaches in order to better address such undertakings.

Our second contribution is a framework, developed with the Coq proof assistant, for reasoning on software architectures: Mefresa. This encompasses the mechanization of the GCM specification, and the means to reason about reconfigurable GCM architectures. Further, we address behavioural concerns by formalizing a semantics based on execution traces of synchronized transition systems. Overall, it provides the first steps towards a complete specification and verification platform addressing both architectural and behavioural properties.


Finally, our third contribution is a new Architecture Description Language (ADL), denominated Painless. Moreover, we discuss its proof-of-concept integration with ProActive — a Java middleware for concurrent and distributed programming, and the de facto reference implementation of the GCM. Painless allows to specify parametrized GCM architectures, along with their structural reconfigurations, in a declarative-like language. Compliance with the GCM specification is evaluated by certified functional code extracted from Mefresa. This permits the safe deployment and reconfiguration of GCM applications.

Cristian Ruz: Autonomic Components and Machine Learning, a couple of perspectives

Mercredi 26 Novembre 2014

In this talk I’ll present our last advances regarding implementation of autonomic behaviour in GCM components through an autonomic load balancer, in the context of the SCADA associate team ( Second, I’ll summarize some of the activities I’ve been involved in the context of the GRIMA research group ( and how autonomic components technology may help to process big sources of data as they are used for machine learning tasks.

Round Table 2014-11-28

  • Maéva Antoine
    • Dealing with Skewed Data in Structured Overlays using Variable Hash Functions (PDCAT’14) [slides]
  • Vincenzo Mastandrea
    • Deadlock Analysis of Asynchronous Sequential Processes (Master thesis) [slides]

Soutenance de thèse de Yanwen CHEN// Phd Defense on the 30th of November 2014 at 3.00 pm at SHANGHAI, EAST CHINA NORMAL UNIVERSITY

Un modèle de comportement temporisé pour les systèmes distribué communicants

A timed Communication behaviour model for Distributed systems

Round Table 2014-10-17

  • Maéva Antoine
    • A Generic API for Load Balancing in Structured P2P Systems (WPBA’14)  [slides]