Symbolic verification of real-time design patterns

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.

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 A1A2 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”.

Reference

  1. 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. [ bib | DOI ]

Leave a Reply

Your email address will not be published. Required fields are marked *