This proposal focuses on the extension of the theory of BIP design patterns (called “architectures”) to the real-time domain.
Context
In our previous paper [1], 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 A1 and A2 enforce respectively safety properties (intuitively: “something bad will never happen”) Φ1 and Φ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.
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”.