Composability & verification of BIP design patterns

sbliudze

This proposal focuses on the implementation and extension of the results presented in a recent paper on the verification of BIP design patterns with data.

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 the 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 objectives

The objectives of this project are twofold, consisting of a theoretical and an implementation part, both aiming to extend the results of [1]. Thus, depending on the students’ profiles and motivation, this proposal can be the subject of 1 or 2 internships.

Theoretical part

  1. Propose conditions sufficient for the composability results of [1] to be extended to more general kinds of priority
  2. Study conditions for the preservation of liveness properties (intuitively: “something good will eventually happen“)

Implementation part

  1. Using the BIP metamodel designed in the Eclipse Modeling Framework (EMF), implement and evaluate a tool realising the BIP-to-pNets encoding presented in the paper
  2. Implement an SMT-based tool for checking the conditions for the preservation of liveness properties and of safety properties in the presence of priorities

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 patterns 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 ]