Conference
A Formal Link Between Response Time Analysis and Network Calculus
| العنوان: | A Formal Link Between Response Time Analysis and Network Calculus |
|---|---|
| المؤلفون: | Roux, Pierre, Quinton, Sophie, Boyer, Marc |
| المساهمون: | DTIS, ONERA, Université de Toulouse Toulouse, ONERA-PRES Université de Toulouse, Sound Programming of Adaptive Dependable Embedded Systems (SPADES), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP), Université Grenoble Alpes (UGA), ARNRT-Proofs, European Project |
| المصدر: | ECRTS 2022 - 34th Euromicro Conference on Real-Time Systems ; https://hal.science/hal-03770727 ; ECRTS 2022 - 34th Euromicro Conference on Real-Time Systems, Jul 2022, Modene, Italy. ⟨10.4230/LIPIcs.ECRTS.2022.5⟩ |
| بيانات النشر: | HAL CCSD Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| سنة النشر: | 2022 |
| المجموعة: | Université Grenoble Alpes: HAL |
| مصطلحات موضوعية: | Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq, Computer systems organization → Real-time system specification, Networks → Formal specifications, Software and its engineering → Formal methods, General and reference → Verification, [SPI]Engineering Sciences [physics] |
| جغرافية الموضوع: | Modene, Italy |
| الوصف: | International audience ; Classical Response Time Analysis (RTA) and Network Calculus (NC) are two major formalisms used for the verification of real-time properties. We offer mathematical links between these two different theories. Based on these links, we then prove the equivalence of various key notions in both frameworks. This enables specialists of both formalisms to get increase confidence on their models, or even, like the authors, to discover errors in theorems by investigating apparent discrepancies between some notions expected to be equivalent. The presented mathematical results are all mechanically checked with the interactive theorem prover Coq, building on existing formalizations of RTA and NC. Establishing such a link between NC and RTA paves the way for improved real-time analyses obtained by combining both theories to enjoy their respective strengths (e.g., multicore analyses for RTA or clock drifts for NC). |
| نوع الوثيقة: | conference object |
| اللغة: | English |
| DOI: | 10.4230/LIPIcs.ECRTS.2022.5 |
| الاتاحة: | https://hal.science/hal-03770727 https://hal.science/hal-03770727v1/document https://hal.science/hal-03770727v1/file/DTIS22153.pdf https://doi.org/10.4230/LIPIcs.ECRTS.2022.5 |
| Rights: | http://creativecommons.org/licenses/by/ ; info:eu-repo/semantics/OpenAccess |
| رقم الانضمام: | edsbas.7C721DD6 |
| قاعدة البيانات: | BASE |
| DOI: | 10.4230/LIPIcs.ECRTS.2022.5 |
|---|