Home > Archives > RSD (Archive) > Research Topics > Correct-by-Construction Implementation Techniques

Real-Time Implementation

Real-Time Implementations of BIP Models

This activity focuses on providing real-time implementations of BIP applications.

Sommaire

1 2 3

Real-Time

The behavior layer of BIP is extended to timed automata (and timed Petri nets). We consider discrete time semantics for clocks and urgency types (i.e. lazy, delayable, or eager [1]) for transitions. Our methodology relies on two models of the application [2]:

The abstract model is defined without considering a specific execution platform. It provides timing constraints for transitions that are only user requirements, and it considers instantaneous interactions execution.
Given execution times for interactions, the abstract model is modified into a corresponding physical model such as to take into account platform characteristics. A physical model is time-safe (i.e. deadlines are met) if its execution traces are included in the execution traces of the abstract model. It is time-robust if reducing the execution times preserves this property.

We implemented a Real-Time BIP Execution Engine that performs the real-time execution of BIP programs on a target platform, that is, execution times are obtained from the actual execution of the interactions on the platform, using a real-time clock of the target platform. It also checks for time-safety violation during the execution when time-robustness cannot be guaranteed for worst-case execution times.

1 2 3

[1] S. Bornot and J. Sifakis. An algebraic framework for urgency. Inf. Comput., 163(1):172—202, 2000.

[2] T. Abdellatif, J. Combaz, J. Sifakis. Model-Based Implementation of Real-Time Applications. In Proceedings of the 10th Conference on Embedded Software (EMSOFT 2010).