In our previous paper , we have defined the notion of architectures—design patterns for the BIP component-based framework.
An architecture is as an operator
A that, applied to a set of components
B, builds a composite component
A(B) meeting a characteristic property
Φ. Composability is based on an associative, commutative and idempotent architecture composition operator
⊕. Both the notion of architectures and the composition operator
⊕ are formally defined within the context of the BIP framework.
The main result is that if two architectures
A2 enforce respectively safety properties (intuitively: “something bad will never happen”)
Φ2, the composed architecture
A1 ⊕ A2 enforces the property
Φ1 ∧ Φ2, that is both properties are preserved by architecture composition. We have, furthermore, defined the notion of non-interference and proved that, if two architectures are mutually non-interfering, their composition also preserves liveness properties (intuitively: “something good will eventually happen”).
During his internship, Waïss has extended these results to the real-time domain (relying on timed automata as the behavioural model). However, checking non-interference of real-time architectures turned out to be a computationally expensive task.
The project objectives
The goal of this project is to propose and implement abstractions and symbolic methods allowing efficient non-interference verification, e.g. using Satisfiability Modulo Theories (SMT) solvers. Location
The internship will be carried out in the Spirals project team at Inria Lille – Nord Europe.
Contact and application
For additional information and to apply please send me an e-mail (in English or French) with the subject “Real-time design patterns internship”.
- Paul Attie, Eduard Baranov, Simon Bliudze, Mohamad Jaber, and Joseph Sifakis. A general framework for architecture composability. Formal Aspects of Computing, 18(2):207–231, April 2016. Open access. [ DOI ]