M2R Research Internship - I/O Types for 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], 
that subsumes located variants of the pi-calculus [2], and more abstract computational models such as Milner's bigraphs [3].

Subject of the internship

The original Location Graphs model has only a crude notion of types and does not exploit it fully
to constrain the behavior of component graphs and capture architectural constraints that may occur in dynamic software systems. 
The goal of this internship is to develop a simple type system for Location Graphs, inspired by notions of i/o types
for the pi-calculus [4] and by mobility types in Boxed Ambients [5], 
that takes advantage of operations available in a location graph (communication,
passivation, and graph modification) to prevent simple forms of errors, including classical communicaton errors but
also less classical reconfiguration errors such as unlawful node update, binding and movement. If sucessful, 
the internship can begin to investigate more complex forms of types dealing with graph-based architectural conditions 
such as encapsulation and dependency invariants. The internship can lead to publication and/or a PhD on the topic of
type systems for 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] D. Sangiorgi, D. Walker : "The pi-calculus: A Theory of Mobile Processes", Cambridge University Press, 2001.

[5] M. Bugliesi, S. Crafa, M. Merro, V. Sassone: "Communication and mobility control in boxed ambients", 
Information and Computation 202(1), 2005.



Contact

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