Hybrid Latency Minimization Approach Using Model Checking and Dataflow Analysis

Guus Kuiper, Philip Sebastian Kurtin, Marco Jan Gerrit Bekooij

    Research output: Contribution to conferencePaper

    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 conferencePaper

    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