M2R Research Internship -  Reversibility and Compensation in Location Graphs

Scientific context

Location Graphs are a new formal model for component-based systems currently developed in the INRIA SPADES team,
that combines concurrent composition, dynamic reconfiguration and graph-like component structures [1].
The Location Graphs model subsumes previous computational models for mobile and distributed systems including
distributed or located variants of Milner's pi-calculus [2], and more abstract computational models such as Milner's bigraphs [3].

Subject of the internship

Compensations are a basic mechanism for fault recovery, which have been the subject of several recent works, e.g. [6,7].
The goal of this internship is to study the introduction of compensation mechanisms in the Location Graphs model,
allowing the possibility for compensations to rollback to well-defined previous states. To progress towards that goal, 
the internship will first study the relationship between the primitives for controlled rollback introduced in [5]
and the primitives for dynamic compensation studied in [7]. In a second phase, it will study introducing causally consistent
reversibility and compensation capabilities in Location Graphs. The internship can lead to publication and/or a PhD on the topic of
fault-recovery in dynamic software architectures.


References

[1] J.B. Stefani : "Component as location graphs", in Proc. 11th Int. Symp. Formal Aspects of Component Software (FACS), 
LNCS 8997, Springer, 2015.

[2] R. Milner : "Communicating and Mobile Systems: The Pi Calculus", Cambridge University Press, 1999.

[3] R. Milner : "The Space and Motion of Communicating Agents", Cambridge University Press, 2009.

[4] I. Lanese, C.A. Mezzina, J.B. Stefani: "Reversing Higher-Order Pi", in Proc. CONCUR, LNCS 6269, Springer, 2010.

[5] I. Lanese, C.A. Mezzina, A. Schmitt, J.B. Stefani: "Concurrent Flexible Reversibility", in Proc. ESOP,
LNCS 7792, Springer, 2013.

[6] R. Bruni, H. C. Melgratti, U. Montanari: "Theoretical foundations for compensations in flow composition languages",
in proc. 32nd POPL, 2005.

[7] I. Lanese, C. Vaz, C. Ferreira: "On the Expressive Power of Primitives for Compensation Handling", in proc. ESOP,
LNCS 6012, Springer, 2010.


Contact

Jean-Bernard Stefani, INRIA SPADES team, jean-bernard.stefani@inria.fr