Context

In a recent paper [1], we have presented some composability results for BIP design patterns (“architectures“) with data (see the figure below for an example) and maximal progress priorities. These results allow simultaneous application of several such architectures enforcing different safety properties (intuitively: “something bad will never happen“), guaranteeing that all these properties will hold in the composed system. We have also provided an encoding into another formalism, pNets, which allows verification of individual architectures using an SMT-based approach.

Example of a BIP architecture: Failure monitor

The project objective

The objective of this project is to implement and extend the results of this paper:

  1. Implement a tool realising the BIP-to-pNets encoding presented in the paper, using the BIP metamodel designed in the Eclipse Modeling Framework (EMF)
  2. Propose conditions sufficient for the composability results of [1] to be extended to more general kinds of priority
  3. Implement an SMT-based tool to check these conditions
  4. (If time permits) Study conditions for the preservation of liveness properties (intuitively: “something good will eventually happen“)

Location

The internship will be carried out in the Spirals project team at Inria Lille – Nord Europe under joint supervision by Simon Bliudze and Eric Madelaine (Inria Sophia Antipolis – Mediterranée).

Contact and application

For additional information and to apply please send me an e-mail (in English or French) with the subject “BIP design partners internship”.

Reference

  1. Simon Bliudze, Ludovic Henrio, and Eric Madelaine. Verification of concurrent design patterns with data. In Proc. of the 21st International Conference on Coordination Models and Languages (COOORDINATION 2019), volume 11533 of LNCS, page 161–181. Springer, June 2019. PDF