4 Search Results for "Lipari, Giuseppe"

Document
Artifact
DOI: 10.4230/DARTS.9.1.4
From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact)

Authors: Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan M. Rivas, and Youcheng Sun

Published in: DARTS, Volume 9, Issue 1, Special Issue of the 35th Euromicro Conference on Real-Time Systems (ECRTS 2023)

Abstract
We propose here solutions to the FMTV 2015 challenge of a distributed video processing system using four different formalisms, as well as the description of the challenge itself. This artifact contains several solutions to various subchallenges, and instructions and scripts to reproduce these results smoothly.
Cite as

Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan M. Rivas, and Youcheng Sun. From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact). In Special Issue of the 35th Euromicro Conference on Real-Time Systems (ECRTS 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 1, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{altmeyer_et_al:DARTS.9.1.4,
  author =	{Altmeyer, Sebastian and Andr\'{e}, \'{E}tienne and Dal Zilio, Silvano and Fejoz, Lo\"{i}c and Harbour, Michael Gonz\'{a}lez and Graf, Susanne and Guti\'{e}rrez, J. Javier and Henia, Rafik and Le Botlan, Didier and Lipari, Giuseppe and Medina, Julio and Navet, Nicolas and Quinton, Sophie and Rivas, Juan M. and Sun, Youcheng},
  title =	{{From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact)}},
  pages =	{4:1--4:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{1},
  editor =	{Altmeyer, Sebastian and Andr\'{e}, \'{E}tienne and Dal Zilio, Silvano and Fejoz, Lo\"{i}c and Harbour, Michael Gonz\'{a}lez and Graf, Susanne and Guti\'{e}rrez, J. Javier and Henia, Rafik and Le Botlan, Didier and Lipari, Giuseppe and Medina, Julio and Navet, Nicolas and Quinton, Sophie and Rivas, Juan M. and Sun, Youcheng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.9.1.4},
  URN =		{urn:nbn:de:0030-drops-180257},
  doi =		{10.4230/DARTS.9.1.4},
  annote =	{Keywords: Verification challenge, industrial use case, end-to-end latency, real-time systems, response time analysis}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.ECRTS.2023.19
From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Invited Paper)

Authors: Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan M. Rivas, and Youcheng Sun

Published in: LIPIcs, Volume 262, 35th Euromicro Conference on Real-Time Systems (ECRTS 2023)

Abstract
We present here the main features and lessons learned from the first edition of what has now become the ECRTS industrial challenge, together with the final description of the challenge and a comparative overview of the proposed solutions. This verification challenge, proposed by Thales, was first discussed in 2014 as part of a dedicated workshop (FMTV, a satellite event of the FM 2014 conference), and solutions were discussed for the first time at the WATERS 2015 workshop. The use case for the verification challenge is an aerial video tracking system. A specificity of this system lies in the fact that periods are constant but known with a limited precision only. The first part of the challenge focuses on the video frame processing system. It consists in computing maximum values of the end-to-end latency of the frames sent by the camera to the display, for two different buffer sizes, and then the minimum duration between two consecutive frame losses. The second challenge is about computing end-to-end latencies on the tracking and camera control for two different values of jitter. Solutions based on five different tools - Fiacre/Tina, CPAL (simulation and analysis), IMITATOR, UPPAAL and MAST - were submitted for discussion at WATERS 2015. While none of these solutions provided a full answer to the challenge, a combination of several of them did allow to draw some conclusions.
Cite as

Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan M. Rivas, and Youcheng Sun. From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Invited Paper). In 35th Euromicro Conference on Real-Time Systems (ECRTS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 262, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{altmeyer_et_al:LIPIcs.ECRTS.2023.19,
  author =	{Altmeyer, Sebastian and Andr\'{e}, \'{E}tienne and Dal Zilio, Silvano and Fejoz, Lo\"{i}c and Harbour, Michael Gonz\'{a}lez and Graf, Susanne and Guti\'{e}rrez, J. Javier and Henia, Rafik and Le Botlan, Didier and Lipari, Giuseppe and Medina, Julio and Navet, Nicolas and Quinton, Sophie and Rivas, Juan M. and Sun, Youcheng},
  title =	{{From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS}},
  booktitle =	{35th Euromicro Conference on Real-Time Systems (ECRTS 2023)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-280-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{262},
  editor =	{Papadopoulos, Alessandro V.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2023.19},
  URN =		{urn:nbn:de:0030-drops-180486},
  doi =		{10.4230/LIPIcs.ECRTS.2023.19},
  annote =	{Keywords: Verification challenge, industrial use case, end-to-end latency}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2019.24
A Bandwidth Reservation Mechanism for AXI-Based Hardware Accelerators on FPGAs

Authors: Marco Pagani, Enrico Rossi, Alessandro Biondi, Mauro Marinoni, Giuseppe Lipari, and Giorgio Buttazzo

Published in: LIPIcs, Volume 133, 31st Euromicro Conference on Real-Time Systems (ECRTS 2019)

Abstract
Hardware platforms for real-time embedded systems are evolving towards heterogeneous architectures comprising different types of processing cores and dedicated hardware accelerators, which can be implemented on silicon or dynamically deployed on FPGA fabric. Such accelerators typically access a shared memory to exchange a significant amount of data with other processing elements. Existing COTS solutions focus on maximizing the overall throughput of the system, rather than guaranteeing the timing constraints of individual hardware accelerators. This paper presents the AXI budgeting unit (ABU), a hardware-based solution to implement a bandwidth reservation mechanism on top of the AMBA AXI standard infrastructure for hardware accelerators deployed on FPGAs. An accurate and tractable model, as well as the corresponding analysis, are also proposed to bound the response time of hardware accelerators in the presence of ABUs, in order to verify whether they can complete before their deadlines. Finally, a set of experiments are reported to evaluate the proposed approach on a state-of-the-art platform, namely the Zynq-7020 by Xilinx. The resource consumption of the ABU has been quantified to be less than 1% of the total FPGA resources of the Zynq-7020.
Cite as

Marco Pagani, Enrico Rossi, Alessandro Biondi, Mauro Marinoni, Giuseppe Lipari, and Giorgio Buttazzo. A Bandwidth Reservation Mechanism for AXI-Based Hardware Accelerators on FPGAs. In 31st Euromicro Conference on Real-Time Systems (ECRTS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 133, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{pagani_et_al:LIPIcs.ECRTS.2019.24,
  author =	{Pagani, Marco and Rossi, Enrico and Biondi, Alessandro and Marinoni, Mauro and Lipari, Giuseppe and Buttazzo, Giorgio},
  title =	{{A Bandwidth Reservation Mechanism for AXI-Based Hardware Accelerators on FPGAs}},
  booktitle =	{31st Euromicro Conference on Real-Time Systems (ECRTS 2019)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-110-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{133},
  editor =	{Quinton, Sophie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2019.24},
  URN =		{urn:nbn:de:0030-drops-107611},
  doi =		{10.4230/LIPIcs.ECRTS.2019.24},
  annote =	{Keywords: AXI Bus, Bandwidth Reservation, Hardware Acceleration, FPGA}
}
Document
DOI: 10.4230/OASIcs.WCET.2015.55
Context-sensitive Parametric WCET Analysis

Authors: Clément Ballabriga, Julien Forget, and Giuseppe Lipari

Published in: OASIcs, Volume 47, 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)

Abstract
In this paper, we propose aWCET analysis that focuses on two aspects. First, it supports contextsensitive hardware and software timing effects, meaning that it is sensitive to the execution history of the program and thus can account for effects like cache persistence, triangular loop, etc. Second, it supports the introduction of parameters in both the software model (e.g. parametric loop bounds) and the hardware model (e.g. number of cache misses). WCET computation by static analysis is traditionally handled by the Implicit Path Enumeration Technique (IPET), using an Integer Linear Program (ILP) that is difficult to resolve parametrically. We suggest an alternative tree-based approach. We define a context-sensitive CFG format to express these effects, and we provide an efficient method to process it, giving a parametric WCET formula. Experimental results show that this new method is significantly faster and more accurate than existing parametric approaches.
Cite as

Clément Ballabriga, Julien Forget, and Giuseppe Lipari. Context-sensitive Parametric WCET Analysis. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 55-64, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{ballabriga_et_al:OASIcs.WCET.2015.55,
  author =	{Ballabriga, Cl\'{e}ment and Forget, Julien and Lipari, Giuseppe},
  title =	{{Context-sensitive Parametric WCET Analysis}},
  booktitle =	{15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
  pages =	{55--64},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-95-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{47},
  editor =	{Cazorla, Francisco J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.55},
  URN =		{urn:nbn:de:0030-drops-52569},
  doi =		{10.4230/OASIcs.WCET.2015.55},
  annote =	{Keywords: Parametric, WCET, Real-time, Static analysis}
}
  • Refine by Author
  • 4 Lipari, Giuseppe
  • 2 Altmeyer, Sebastian
  • 2 André, Étienne
  • 2 Dal Zilio, Silvano
  • 2 Fejoz, Loïc
  • Show More...

  • Refine by Classification
  • 3 Computer systems organization → Real-time systems
  • 2 Computer systems organization → Embedded systems
  • 2 General and reference → Verification
  • 2 Software and its engineering → Software verification and validation
  • 1 Computer systems organization → System on a chip
  • Show More...

  • Refine by Keyword
  • 2 Verification challenge
  • 2 end-to-end latency
  • 2 industrial use case
  • 1 AXI Bus
  • 1 Bandwidth Reservation
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2023
  • 1 2015
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact