This proposal 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 a previous ENS L3 internship, Waïss Azizian 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”.