Search Results

Documents authored by Boyer, Marc

Document
DOI: 10.4230/LIPIcs.ECRTS.2024.9
Switching Between Left and Right Continuity in Network Calculus

Authors: Damien Guidolin--Pina and Marc Boyer

Published in: LIPIcs, Volume 298, 36th Euromicro Conference on Real-Time Systems (ECRTS 2024)

Abstract
The Network Calculus theory has been designed to compute upper bounds on delay and backlog in data networks. A lot of results have been developed to address different aspects. However, they are not all compatible with each other since they make different assumptions on the continuity of a core aspect of the model (the cumulative curves). However, real systems may mix several mechanisms. When modeling such a system, one has to choose one continuity hypothesis and limit the analysis to a subset of existing results. This paper addresses the continuity problem and argues formally that continuity issues are mathematical details that can be solved as long as the min-plus properties are used (minimal and maximal service, shaping). Conversely, it gives a counter-example for properties based on strict service, requiring a generalisation of the backlogged interval notion.
Cite as

Damien Guidolin--Pina and Marc Boyer. Switching Between Left and Right Continuity in Network Calculus. In 36th Euromicro Conference on Real-Time Systems (ECRTS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 298, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guidolinpina_et_al:LIPIcs.ECRTS.2024.9,
  author =	{Guidolin--Pina, Damien and Boyer, Marc},
  title =	{{Switching Between Left and Right Continuity in Network Calculus}},
  booktitle =	{36th Euromicro Conference on Real-Time Systems (ECRTS 2024)},
  pages =	{9:1--9:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-324-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{298},
  editor =	{Pellizzoni, Rodolfo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2024.9},
  URN =		{urn:nbn:de:0030-drops-203129},
  doi =		{10.4230/LIPIcs.ECRTS.2024.9},
  annote =	{Keywords: Worst-case analysis, Real-time and embedded systems, Network Calculus}
}
Document
DOI: 10.4230/LITES.9.1.1
Equivalence between the Urgency Based Shaper and Asynchronous Traffic Shaping in Time Sensitive Networking

Authors: Marc Boyer

Published in: LITES, Volume 9, Issue 1 (2024). Leibniz Transactions on Embedded Systems, Volume 9, Issue 1

Abstract
The Asynchronous Traffic Shaping (ATS) has been designed by the Time Sensitive Networking (TSN) group as a reshaping mechanism for real-time data flows, based on the initial proposition of the Urgency Based Shaper (UBS). Several studies have exhibited properties and limitations of this solution, but most of them are based on the model presented in the UBS definition [Specht and Samii, 2016], whereas the implementation described in the standard uses a different architecture and algorithm. This paper presents an equivalence proof between the model and the standard specification.
Cite as

Marc Boyer. Equivalence between the Urgency Based Shaper and Asynchronous Traffic Shaping in Time Sensitive Networking. In LITES, Volume 9, Issue 1 (2024). Leibniz Transactions on Embedded Systems, Volume 9, Issue 1, pp. 1:1-1:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{boyer:LITES.9.1.1,
  author =	{Boyer, Marc},
  title =	{{Equivalence between the Urgency Based Shaper and Asynchronous Traffic Shaping in Time Sensitive Networking}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{1:1--1:27},
  ISSN =	{2199-2002},
  year =	{2024},
  volume =	{9},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.9.1.1},
  URN =		{urn:nbn:de:0030-drops-198271},
  doi =		{10.4230/LITES.9.1.1},
  annote =	{Keywords: TSN, Time Sensitive Networking, ATS, Asynchronous Traffic Shaping, 802.1Qcr}
}
Document
Artifact
DOI: 10.4230/DARTS.8.1.3
A Formal Link Between Response Time Analysis and Network Calculus (Artifact)

Authors: Pierre Roux, Sophie Quinton, and Marc Boyer

Published in: DARTS, Volume 8, Issue 1, Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)

Abstract
Classical Response Time Analysis (RTA) and Network Calculus (NC) are two major formalisms used for the verification of real-time properties. The related paper offer mathematical links between these two different theories. Based on these links, it then proves 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). This artifact enables to reproduce these proofs.
Cite as

Pierre Roux, Sophie Quinton, and Marc Boyer. A Formal Link Between Response Time Analysis and Network Calculus (Artifact). In Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 1, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{roux_et_al:DARTS.8.1.3,
  author =	{Roux, Pierre and Quinton, Sophie and Boyer, Marc},
  title =	{{A Formal Link Between Response Time Analysis and Network Calculus (Artifact)}},
  pages =	{3:1--3:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{1},
  editor =	{Roux, Pierre and Quinton, Sophie and Boyer, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.1.3},
  URN =		{urn:nbn:de:0030-drops-164990},
  doi =		{10.4230/DARTS.8.1.3},
  annote =	{Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2022.5
A Formal Link Between Response Time Analysis and Network Calculus

Authors: Pierre Roux, Sophie Quinton, and Marc Boyer

Published in: LIPIcs, Volume 231, 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)

Abstract
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).
Cite as

Pierre Roux, Sophie Quinton, and Marc Boyer. A Formal Link Between Response Time Analysis and Network Calculus. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 231, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{roux_et_al:LIPIcs.ECRTS.2022.5,
  author =	{Roux, Pierre and Quinton, Sophie and Boyer, Marc},
  title =	{{A Formal Link Between Response Time Analysis and Network Calculus}},
  booktitle =	{34th Euromicro Conference on Real-Time Systems (ECRTS 2022)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-239-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{231},
  editor =	{Maggio, Martina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2022.5},
  URN =		{urn:nbn:de:0030-drops-163224},
  doi =		{10.4230/LIPIcs.ECRTS.2022.5},
  annote =	{Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq}
}
Document
Artifact
DOI: 10.4230/DARTS.7.1.2
A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact)

Authors: Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille

Published in: DARTS, Volume 7, Issue 1, Special Issue of the 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021)

Abstract
Computing response times for resources shared by periodic workloads (tasks or data flows) can be very time consuming as it depends on the least common multiple of the periods. In a previous study, a quadratic algorithm was provided to upper bound the response time of a set of periodic tasks with a fixed-priority scheduling. The related paper generalises this result by considering a rate-latency server and sporadic workloads and gives a response time and residual curve that can be used in other contexts. It also provides a formal proof in the Coq language. This artifact enables to reproduce this proof.
Cite as

Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille. A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact). In Special Issue of the 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 1, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{boyer_et_al:DARTS.7.1.2,
  author =	{Boyer, Marc and Roux, Pierre and Daigmorte, Hugo and Puechmaille, David},
  title =	{{A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact)}},
  pages =	{2:1--2:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{1},
  editor =	{Boyer, Marc and Roux, Pierre and Daigmorte, Hugo and Puechmaille, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.7.1.2},
  URN =		{urn:nbn:de:0030-drops-139810},
  doi =		{10.4230/DARTS.7.1.2},
  annote =	{Keywords: Network Calculus, response time, residual curve, rate-latency server, sporadic workload, formal proof, Coq}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2021.14
A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus

Authors: Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille

Published in: LIPIcs, Volume 196, 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021)

Abstract
Computing response times for resources shared by periodic workloads (tasks or data flows) can be very time consuming as it depends on the least common multiple of the periods. In a previous study, a quadratic algorithm was provided to upper bound the response time of a set of periodic tasks with a fixed-priority scheduling. This paper generalises this result by considering a rate-latency server and sporadic workloads and gives a response time and residual curve that can be used in other contexts. It also provides a formal proof in the Coq language.
Cite as

Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille. A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus. In 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 196, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{boyer_et_al:LIPIcs.ECRTS.2021.14,
  author =	{Boyer, Marc and Roux, Pierre and Daigmorte, Hugo and Puechmaille, David},
  title =	{{A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus}},
  booktitle =	{33rd Euromicro Conference on Real-Time Systems (ECRTS 2021)},
  pages =	{14:1--14:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-192-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{196},
  editor =	{Brandenburg, Bj\"{o}rn B.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2021.14},
  URN =		{urn:nbn:de:0030-drops-139457},
  doi =		{10.4230/LIPIcs.ECRTS.2021.14},
  annote =	{Keywords: Network Calculus, response time, residual curve, rate-latency server, sporadic workload, formal proof, Coq}
}
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact