Axiomatic system for hybrid interactions in JavaBIP

PDF of the proposal

The main goal of this project is to exhibit a set of axioms formalising the equivalence relation on the extended Algebra of Connectors, which is used to model patterns combining synchronous and asynchronous communication in JavaBIP.

Context

This project focuses on JavaBIP [3], which is an open-source Java implementation of the BIP (Behaviour-Interaction-Priority) framework [1,2] for the coordination of concurrent components.

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.

Project goals

In a previous project [4], 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 exhibiting a set of axioms formalising the equivalence 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.

Benefits

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.

Required skills

Good analytical skills will definitely be required. The candidate must have good understanding of Labelled Transition Systems and Finite State Automata.

Location

The internship will be carried out in the Spirals project team at Inria Lille – Nord Europe under supervision by Simon Bliudze.

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 in JavaBIP".

References

  1. 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]
  2. 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]
  3. Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek, and Alina Zolotukhina. Exogenous coordination of concurrent software components with JavaBIP. Software: Practice and Experience47(11):1801–1836, November 2017. [PDF]
  4. Tarcisio Teixeira. Structuring asynchronous interactions in JavaBIP. CSE 303 report, Ecole Polytechnique, December 2020.

Leave a Reply

Your email address will not be published. Required fields are marked *