The main goal of this project is to propose a set of axioms defining the congruence relation on the extended Algebra of Connectors used to model patterns combining synchronous and asynchronous communication in component-based systems.
The concurrent nature of most modern software systems makes the analysis of their behaviour extremely difficult due to the fact that their state space is exponential in the number of components. To address this issue, both BIP and JavaBIP rely on a strong separation between (sequential) computation realised by components and coordination of their concurrent behaviour. Components are modelled as Finite State Machines (FSMs). Transitions of these FSMs are labelled by action names called ports, which form their interfaces. The coordination of component behaviours is defined by connectors that specify which ports must synchronise (i.e. the corresponding transitions must fire together).
Since connectors are defined separately from components, we get an additional benefit: the component systems become modular because the implementation of a component does not depend on the architecture of the system it is used in.
In JavaBIP, we have introduced a distinction between two types of ports: enforceable and spontaneous. Enforceable ports are controllable, i.e. the BIP engine can decide when to fire them. Spontaneous ports are not controllable: they are intended to be used for receiving notifications from the environment. For instance, a component that keeps track of physical device must update its state when the physical conditions evolve. However, it turns out that this mechanism is also useful for asynchronous communication among components: one component can send a message to another as a notification to be received through a spontaneous port. One can also imagine more complex uses, where one component broadcasts a message to several others, several components synchronise to send an aggregated message to another one, etc.
In a previous project , we have defined an extended algebra of connectors to model patterns combining synchronous and asynchronous communication. The goal of this project is to further advance that work by proposing a set of axioms defining the congruence relation on that algebra. Further steps can include, the incorporation of the data transfer mechanism into this algebraic representation and the development of transformation techniques to implement connectors through message exchange protocols.
You will learn the principles of rigorous system design based on formal operational semantics and get an in-depth understanding of BIP, a state-of-the-art component-based framework. Successful internship can lead to a research publication.
Good analytical skills will definitely be required. Prior knowledge of basic algebra is a plus.
Contact and application
For additional information and to apply please send an e-mail to Simon Bliudze (in English or French) with the subject "Axiomatic system for hybrid interactions".
- Simon Bliudze and Joseph Sifakis. The Algebra of Connectors — Structuring interaction in BIP. In Proceedings of the 7th ACM & IEEE International Conference on Embedded Software, EMSOFT 2007, pages 11–20, Salzburg, Austria, October 2007. ACM SigBED. [PDF]
- Ananda Basu, Saddek Bensalem, Marius Bozga, Jacques Combaz, Mohamad Jaber, Thanh-Hung Nguyen, and Joseph Sifakis: Rigorous component-based system design using the BIP framework. IEEE Software 28(3):41–48 (2011) [Website | PDF]
- Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek, and Alina Zolotukhina. Exogenous coordination of concurrent software components with JavaBIP. Software: Practice and Experience, 47(11):1801–1836, November 2017. [PDF]
- Tarcisio Teixeira. Structuring asynchronous interactions in JavaBIP. CSE 303 report, Ecole Polytechnique, December 2020.