Formalism for the high-level design of hard real-time embedded systems

Real-time embedded systems are at the core of modern industrialized societies. They are a privileged target for the application of formal methods. The importance of real-time constraints in the specification of these systems requires the design of ad-hoc solutions. This work considers a class of real-time systems including those developed using OASIS, a tool-chain targeting hard real-time embedded systems developed at CEA LIST. We study the notion of end-to-end delay, which we propose to model as a constraint bearing directly on the influence of the input information flow over the output information flow . In order to cope with the growing complexity of real-time embedded systems, we study the possibility to apply this new notion of delay to the incremental development of such systems, by using both stepwise refinement and composition operators. We define the necessary and sufficient conditions to the preservation of the end-to-end delay by stepwise refinement. Similarly, we give sufficient conditions to compute the end-to-end delay in a compositional fashion. Together, these results permit to establish a formalism allowing to prove end-to-end delay properties in stepwise development methodologies.

Data and Resources

Additional Info

Field Value
Source https://theses.hal.science/tel-00676901
Author Garnier, Ilias
Maintainer CCSD
Last Updated May 25, 2026, 14:22 (UTC)
Created May 25, 2026, 14:22 (UTC)
Identifier NNT: 2012PA112018
Language fr
Rights https://about.hal.science/hal-authorisation-v1/
contributor Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)) ; Direction de Recherche Technologique (CEA) (DRT (CEA)) ; Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)
creator Garnier, Ilias
date 2012-02-10T00:00:00
harvest_object_id 801043cc-f114-4efe-836e-dff704dfd8e7
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2026-03-30T00:00:00
set_spec type:THESE