This proposal builds upon the previous work carried out by Waïss Azizian for his ENS L3 internship project. It focuses on the extension of the theory of BIP design patterns (called “architectures”) to the real-time domain.
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.
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”.