Search Results

Documents authored by André, Étienne

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.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.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
Complete Volume
DOI: 10.4230/OASIcs.SynCoP.2015
OASIcs, Volume 44, SynCoP'15, Complete Volume

Authors: Étienne André and Goran Frehse

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
OASIcs, Volume 44, SynCoP'15, Complete Volume
Cite as

2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{andre_et_al:OASIcs.SynCoP.2015,
  title =	{{OASIcs, Volume 44, SynCoP'15, Complete Volume}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015},
  URN =		{urn:nbn:de:0030-drops-56168},
  doi =		{10.4230/OASIcs.SynCoP.2015},
  annote =	{Keywords: Software/Program Verification}
}
Document
Front Matter
DOI: 10.4230/OASIcs.SynCoP.2015.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Étienne André and Goran Frehse

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. i-xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:OASIcs.SynCoP.2015.i,
  author =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{i--xii},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.i},
  URN =		{urn:nbn:de:0030-drops-56034},
  doi =		{10.4230/OASIcs.SynCoP.2015.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
Informal Presentation
DOI: 10.4230/OASIcs.SynCoP.2015.104
Enhanced Distributed Behavioral Cartography of Parametric Timed Automata (Informal Presentation)

Authors: Étienne André, Camille Coti, and Hoang Gia Nguyen

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
Parametric timed automata (PTA) allow the specification and verification of timed systems incompletely specified, or featuring timing constants that may change either in the design phase, or at runtime. The behavioral cartography of PTA (BC) relies on the idea of covering a bounded parameter domain with tiles, i.e., parts of the parameter domain in which the discrete behavior is uniform. This is achieved by iterating the inverse method (IM) on the (yet uncovered) integer parameter valuations ("points") of the bounded parametric domain: given a reference point, IM generalizes the behavior corresponding to this point by synthesizing a constraint containing other (integer and real-valued) points with the same discrete behavior. Then, given a linear time property, it is easy to partition the parametric domain into a subset of "good" tiles and a subset of "bad" ones (which correspond to good and bad behaviors). Useful applications of BC include the optimization of timing constants, and the measure of the system robustness (values around the reference parameters) w.r.t. the untimed language. In practice, a parameter domain with a large number of integer points will require a long time to compute BC. To alleviate that, our goal is to take advantage of powerful distributed architectures. Distributing BC is theoretically easy, since it is trivial that two executions of IM from two different points can be performed on two different nodes. However, distributing it efficiently is challenging. For example, calling two executions of IM from two contiguous integer points has a large probability to yield the same tile in both cases, resulting in a loss of time for one of the two nodes. Thus, the critical question is how to distribute efficiently the point on which to call IM. In a previous work, a master-worker scheme is proposed, where the master assigns points to each worker process, which is called a point-based distribution scheme. In this point-based distribution scheme, choosing the point distribution approach on the master side is the key point that will decide the algorithm performance. Since the master has no ability to foresee the tiles on cartography (the "shape" of a cartography is unknown in general), two or more processes can receive close points, that then yield the same result, leading to a loss of efficiency. Besides that, two or more tiles can overlap each other; hence, the question is whether we stop an going process starting from a point that is already covered by another tile. Finally, a very large parameter domain (with many integer points) can cause a bottleneck phenomenon on the master side since many worker processes ask for point, while the master is busy to find uncovered points. From the previous problems, we proposed an enhanced master-worker distributed algorithm, based on a domain decomposition scheme. The main idea is that the master splits the parameter domain into subdomains, and assigns them to the workers. Then workers will work on their own set of points, hence reducing the probability of choosing close points since the workers work as far as possible from each other. Then, when a worker finishes the coverage of its subdomain, it asks the master for a new subdomain: the master splits a slow worker's subdomain into two parts, and sends it to the fast worker. Furthermore, we used a heuristic approach to decide whether to stop a process working on a point that has been covered by a tile of another worker. In all our experiments, our enhanced distributed algorithm outperforms previous algorithms.
Cite as

Étienne André, Camille Coti, and Hoang Gia Nguyen. Enhanced Distributed Behavioral Cartography of Parametric Timed Automata (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 104-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:OASIcs.SynCoP.2015.104,
  author =	{Andr\'{e}, \'{E}tienne and Coti, Camille and Nguyen, Hoang Gia},
  title =	{{Enhanced Distributed Behavioral Cartography of Parametric Timed Automata}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{104--105},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.104},
  URN =		{urn:nbn:de:0030-drops-56134},
  doi =		{10.4230/OASIcs.SynCoP.2015.104},
  annote =	{Keywords: Formal methods, model checking, distributed algorithmic, real-time systems, parameter synthesis}
}
Document
DOI: 10.4230/OASIcs.FSFMA.2013.18
Dynamic Clock Elimination in Parametric Timed Automata

Authors: Étienne André

Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)

Abstract
The formalism of parametric timed automata provides designers with a formal way to specify and verify real-time concurrent systems where iming requirements are unknown (or parameters). Such models are usually subject to the state space explosion. A popular way to partially reduce the size of the state space is to reduce the number of clock variables. In this work, we present a technique for dynamically eliminating clocks. Experiments using IMITATOR show a diminution of the number of states and of the computation time, and in some cases allow termination of the analysis of models that could not terminate otherwise. More surprisingly, even when the number of clocks remains constant, there is little noticeable overhead in applying the proposed clock elimination.
Cite as

Étienne André. Dynamic Clock Elimination in Parametric Timed Automata. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 18-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{andre:OASIcs.FSFMA.2013.18,
  author =	{Andr\'{e}, \'{E}tienne},
  title =	{{Dynamic Clock Elimination in Parametric Timed Automata}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{18--31},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.18},
  URN =		{urn:nbn:de:0030-drops-40855},
  doi =		{10.4230/OASIcs.FSFMA.2013.18},
  annote =	{Keywords: Verification, Real-time systems, Parameter synthesis, State space reduction, Inverse Method}
}
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