Hybrid Latency Minimization Approach Using Model Checking and Dataflow Analysis

Guus Kuiper, Philip Sebastian Kurtin, Marco Jan Gerrit Bekooij

Research output: Contribution to conferencePaperAcademicpeer-review

1 Citation (Scopus)
2 Downloads (Pure)

Abstract

Bounding the latency of real-time multiprocessor applications is crucial for safety-critical systems. Several approximative analysis approaches exist that can efficiently analyze the latency. However, these approaches produce pessimistic latency results and do not exploit buffer sizing nor exploit additional sequence constraints to reduce the latency. More accurate latency analysis results can be obtained using model checking of timed-automata, however, at the cost of a typically excessive run-time.

This paper presents a latency analysis approach for cyclic task graphs using model checking of timed automata of which the run-time is reduced. The approach is applicable for systems in which tasks are executed on shared processors using a Fixed Priority Pre-emptive (FPP) scheduling policy. The reduction in run-time is achieved by pruning the search space of options that need to be analyzed using the model checker by making use of approximative dataflow analysis techniques. The approach exploits dimensioning of buffers to minimize interference and latency. Moreover, sequence constraints are introduced and automatically adapted in order to minimize the latency of the task graph.

A WLAN 802.11p transceiver application is used in the case study to compare this hybrid analysis approach to a state-of-the-art approximation based approach that uses iterative buffer sizing. Using our approach, the analyzed latency decreased from 17 μs to 15 μs at the cost of a run-time of 23 minutes instead of a fraction of a second.
Original languageEnglish
Pages41-50
DOIs
Publication statusPublished - Jun 2017
Event20th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2017 - Schloss Rheinfels, Sankt Goar, Germany
Duration: 12 Jun 201713 Jun 2017
Conference number: 20
http://www.scopesconf.org/scopes-17/

Conference

Conference20th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2017
Abbreviated titleSCOPES
CountryGermany
CitySankt Goar
Period12/06/1713/06/17
Internet address

Fingerprint

Data flow analysis
Model checking
Wireless local area networks (WLAN)
Transceivers
Scheduling

Cite this

Kuiper, G., Kurtin, P. S., & Bekooij, M. J. G. (2017). Hybrid Latency Minimization Approach Using Model Checking and Dataflow Analysis. 41-50. Paper presented at 20th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2017, Sankt Goar, Germany. https://doi.org/10.1145/3078659.3078665
Kuiper, Guus ; Kurtin, Philip Sebastian ; Bekooij, Marco Jan Gerrit. / Hybrid Latency Minimization Approach Using Model Checking and Dataflow Analysis. Paper presented at 20th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2017, Sankt Goar, Germany.
@conference{63614796b1e542479a8b83f52e92a5bc,
title = "Hybrid Latency Minimization Approach Using Model Checking and Dataflow Analysis",
abstract = "Bounding the latency of real-time multiprocessor applications is crucial for safety-critical systems. Several approximative analysis approaches exist that can efficiently analyze the latency. However, these approaches produce pessimistic latency results and do not exploit buffer sizing nor exploit additional sequence constraints to reduce the latency. More accurate latency analysis results can be obtained using model checking of timed-automata, however, at the cost of a typically excessive run-time.This paper presents a latency analysis approach for cyclic task graphs using model checking of timed automata of which the run-time is reduced. The approach is applicable for systems in which tasks are executed on shared processors using a Fixed Priority Pre-emptive (FPP) scheduling policy. The reduction in run-time is achieved by pruning the search space of options that need to be analyzed using the model checker by making use of approximative dataflow analysis techniques. The approach exploits dimensioning of buffers to minimize interference and latency. Moreover, sequence constraints are introduced and automatically adapted in order to minimize the latency of the task graph.A WLAN 802.11p transceiver application is used in the case study to compare this hybrid analysis approach to a state-of-the-art approximation based approach that uses iterative buffer sizing. Using our approach, the analyzed latency decreased from 17 μs to 15 μs at the cost of a run-time of 23 minutes instead of a fraction of a second.",
author = "Guus Kuiper and Kurtin, {Philip Sebastian} and Bekooij, {Marco Jan Gerrit}",
year = "2017",
month = "6",
doi = "10.1145/3078659.3078665",
language = "English",
pages = "41--50",
note = "20th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2017, SCOPES ; Conference date: 12-06-2017 Through 13-06-2017",
url = "http://www.scopesconf.org/scopes-17/",

}

Kuiper, G, Kurtin, PS & Bekooij, MJG 2017, 'Hybrid Latency Minimization Approach Using Model Checking and Dataflow Analysis' Paper presented at 20th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2017, Sankt Goar, Germany, 12/06/17 - 13/06/17, pp. 41-50. https://doi.org/10.1145/3078659.3078665

Hybrid Latency Minimization Approach Using Model Checking and Dataflow Analysis. / Kuiper, Guus ; Kurtin, Philip Sebastian; Bekooij, Marco Jan Gerrit.

2017. 41-50 Paper presented at 20th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2017, Sankt Goar, Germany.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

T1 - Hybrid Latency Minimization Approach Using Model Checking and Dataflow Analysis

AU - Kuiper, Guus

AU - Kurtin, Philip Sebastian

AU - Bekooij, Marco Jan Gerrit

PY - 2017/6

Y1 - 2017/6

N2 - Bounding the latency of real-time multiprocessor applications is crucial for safety-critical systems. Several approximative analysis approaches exist that can efficiently analyze the latency. However, these approaches produce pessimistic latency results and do not exploit buffer sizing nor exploit additional sequence constraints to reduce the latency. More accurate latency analysis results can be obtained using model checking of timed-automata, however, at the cost of a typically excessive run-time.This paper presents a latency analysis approach for cyclic task graphs using model checking of timed automata of which the run-time is reduced. The approach is applicable for systems in which tasks are executed on shared processors using a Fixed Priority Pre-emptive (FPP) scheduling policy. The reduction in run-time is achieved by pruning the search space of options that need to be analyzed using the model checker by making use of approximative dataflow analysis techniques. The approach exploits dimensioning of buffers to minimize interference and latency. Moreover, sequence constraints are introduced and automatically adapted in order to minimize the latency of the task graph.A WLAN 802.11p transceiver application is used in the case study to compare this hybrid analysis approach to a state-of-the-art approximation based approach that uses iterative buffer sizing. Using our approach, the analyzed latency decreased from 17 μs to 15 μs at the cost of a run-time of 23 minutes instead of a fraction of a second.

AB - Bounding the latency of real-time multiprocessor applications is crucial for safety-critical systems. Several approximative analysis approaches exist that can efficiently analyze the latency. However, these approaches produce pessimistic latency results and do not exploit buffer sizing nor exploit additional sequence constraints to reduce the latency. More accurate latency analysis results can be obtained using model checking of timed-automata, however, at the cost of a typically excessive run-time.This paper presents a latency analysis approach for cyclic task graphs using model checking of timed automata of which the run-time is reduced. The approach is applicable for systems in which tasks are executed on shared processors using a Fixed Priority Pre-emptive (FPP) scheduling policy. The reduction in run-time is achieved by pruning the search space of options that need to be analyzed using the model checker by making use of approximative dataflow analysis techniques. The approach exploits dimensioning of buffers to minimize interference and latency. Moreover, sequence constraints are introduced and automatically adapted in order to minimize the latency of the task graph.A WLAN 802.11p transceiver application is used in the case study to compare this hybrid analysis approach to a state-of-the-art approximation based approach that uses iterative buffer sizing. Using our approach, the analyzed latency decreased from 17 μs to 15 μs at the cost of a run-time of 23 minutes instead of a fraction of a second.

U2 - 10.1145/3078659.3078665

DO - 10.1145/3078659.3078665

M3 - Paper

SP - 41

EP - 50

ER -

Kuiper G, Kurtin PS, Bekooij MJG. Hybrid Latency Minimization Approach Using Model Checking and Dataflow Analysis. 2017. Paper presented at 20th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2017, Sankt Goar, Germany. https://doi.org/10.1145/3078659.3078665