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.
In a recent paper , 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.
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 . Thus, depending on the students’ profiles and motivation, this proposal can be the subject of 1 or 2 internships.
- Propose conditions sufficient for the composability results of  to be extended to more general kinds of priority
- Study conditions for the preservation of liveness properties (intuitively: “something good will eventually happen“)
- 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
- Implement an SMT-based tool for checking the conditions for the preservation of liveness properties and of safety properties in the presence of priorities
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”.
- 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 ]