CTL
5 juin 2012 - 14h00
Rigorous Implementation of Real-time Systems (Phd Defense)
par Tesnim Abdellatif de Verimag
Abstract: Real-time systems are systems that are subject to real-time constraints? e.g. operational deadlines from event to system response. Building real-time systems
requires the use of design and implementation methodologies that ensure the property of meeting timing constraints e.g. a system has to react within user-defined bounds such as deadlines and periodicity.
We provide a rigorous design and implementation method for real-time systems. The implementation is generated from a given real-time application software and a target platform by using two models:
1) An abstract model representing the behavior of real-time software as a timed automaton. The latter describes user-deined platform-independent timing constraints. Its transitions are timeless and correspond to the execution of statements of the real-time software.
2) A physical model representing the behavior of the real-time software running on a given platform. It is obtained by assigning execution times to the transitions of the abstract model.
A necessary condition for implementability is time-safety, that is, any (timed) execution sequence of the physical model is also an execution sequence of the abstract model. Time-safety means that the platform is fast enough to meet the timing requirements. As execution times of actions are not known exactly, time-safety is checked for worst-case execution times of actions by making an assumption of time-robustness: time-safety is preserved when speed of the execution platform increases.
For given real-time software and execution platform corresponding to a time-robust model, we define an execution engine that coordinates the
execution of the application software so as to meet its timing constraints. Furthermore, in case of non-robustness, the execution engine can detect violations of time-safety and stop execution. We have implemented the execution engine for BIP programs with real-time constraints. We have validated the method for a robotic application implemented on the Dala rover platform. We show the benefits obtained in terms of CPU utilization and amelioration in the latency of reaction.
Jury:
- Prof. Sanjoy Baruah, University of North Carolina, Rapporteur
- Prof. Eugene Asarin, Université Paris Diderot - Paris 7, Rapporteur
- Prof. Roland Groz, INPG, Examinateur
- Prof. Wang YI, Uppsala University, Examinateur
- Dr. Félix Ingrand, LAAS-CNRS, Examinateur
- Prof. Joseph Sifakis, Verimag-CNRS/EPFL, Directeur de these
- Dr. Jacques Combaz, Verimag-CNRS, Co-Directeur de these
