Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems

Publikation: Forskning - peer reviewKonferencebidrag i proceedings

Standard

Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems. / Madzar, Boris; Boudjadar, Jalil; Dingel, Juergen ; Fuhrman, Thomas; S, Ramesh.

Formal Aspects of Component Software. Springer Link, 2017. s. 153-171.

Publikation: Forskning - peer reviewKonferencebidrag i proceedings

Harvard

Madzar, B, Boudjadar, J, Dingel, J, Fuhrman, T & S, R 2017, Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems. i Formal Aspects of Component Software. Springer Link, Lecture Notes in Computer Science LNCS, bind. 10231, s. 153-171, Besancon, Frankrig, 19/10/2016.

APA

Madzar, B., Boudjadar, J., Dingel, J., Fuhrman, T., & S, R. (2017). Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems. I Formal Aspects of Component Software (s. 153-171). Springer Link. Lecture Notes in Computer Science LNCS, Bind. 10231

CBE

Madzar B, Boudjadar J, Dingel J, Fuhrman T, S R. 2017. Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems. I Formal Aspects of Component Software. Springer Link. s. 153-171. (Lecture Notes in Computer Science LNCS, Bind 10231).

MLA

Madzar, Boris o.a.. "Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems". Formal Aspects of Component Software. Springer Link. (Lecture Notes in Computer Science LNCS, Bind 10231). 2017. 153-171.

Vancouver

Madzar B, Boudjadar J, Dingel J, Fuhrman T, S R. Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems. I Formal Aspects of Component Software. Springer Link. 2017. s. 153-171. (Lecture Notes in Computer Science LNCS, Bind 10231).

Author

Madzar, Boris ; Boudjadar, Jalil ; Dingel, Juergen ; Fuhrman, Thomas ; S, Ramesh. / Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems. Formal Aspects of Component Software. Springer Link, 2017. s. 153-171 (Lecture Notes in Computer Science LNCS, Bind 10231).

Bibtex

@inbook{6ecf9ac9b8d34132b4a66af057745230,
title = "Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems",
abstract = "The need to integrate large and complex functions into today’s vehicle electronic control systems requires high performance computing platforms, while at the same time the manufacturers try to reduce cost, power consumption and ensure safety. Traditionally, safety isolation and fault containment of software tasks have been achieved by either physically or temporally segregating them. This approach is reliable but inefficient in terms of processor utilization. Dynamic approaches that achieve better utilization without sacrificing safety isolation and fault containment appear to be of increasing interest. One of these approaches relies on predictable data flow introduced in PharOS and Giotto. In this paper, we extend the work on leveraging predictable data flow by addressing the problem of how the predictability of data flow can be proved formally for mixed criticality systems that run on multicore platforms and are subject to failures. We consider dynamic tasks where the timing attributes vary from one period to another. Our setting also allows for sporadic deadline overruns and accounts for criticality during fault handling. A user interface was created to allow automatic generation of the models as well as visualization of the analysis results, whereas predictability is verified using the Spin model checker.",
author = "Boris Madzar and Jalil Boudjadar and Juergen Dingel and Thomas Fuhrman and Ramesh S",
year = "2017",
month = "4",
pages = "153--171",
booktitle = "Formal Aspects of Component Software",
publisher = "Springer Link",

}

RIS

TY - GEN

T1 - Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems

AU - Madzar,Boris

AU - Boudjadar,Jalil

AU - Dingel,Juergen

AU - Fuhrman,Thomas

AU - S,Ramesh

PY - 2017/4/13

Y1 - 2017/4/13

N2 - The need to integrate large and complex functions into today’s vehicle electronic control systems requires high performance computing platforms, while at the same time the manufacturers try to reduce cost, power consumption and ensure safety. Traditionally, safety isolation and fault containment of software tasks have been achieved by either physically or temporally segregating them. This approach is reliable but inefficient in terms of processor utilization. Dynamic approaches that achieve better utilization without sacrificing safety isolation and fault containment appear to be of increasing interest. One of these approaches relies on predictable data flow introduced in PharOS and Giotto. In this paper, we extend the work on leveraging predictable data flow by addressing the problem of how the predictability of data flow can be proved formally for mixed criticality systems that run on multicore platforms and are subject to failures. We consider dynamic tasks where the timing attributes vary from one period to another. Our setting also allows for sporadic deadline overruns and accounts for criticality during fault handling. A user interface was created to allow automatic generation of the models as well as visualization of the analysis results, whereas predictability is verified using the Spin model checker.

AB - The need to integrate large and complex functions into today’s vehicle electronic control systems requires high performance computing platforms, while at the same time the manufacturers try to reduce cost, power consumption and ensure safety. Traditionally, safety isolation and fault containment of software tasks have been achieved by either physically or temporally segregating them. This approach is reliable but inefficient in terms of processor utilization. Dynamic approaches that achieve better utilization without sacrificing safety isolation and fault containment appear to be of increasing interest. One of these approaches relies on predictable data flow introduced in PharOS and Giotto. In this paper, we extend the work on leveraging predictable data flow by addressing the problem of how the predictability of data flow can be proved formally for mixed criticality systems that run on multicore platforms and are subject to failures. We consider dynamic tasks where the timing attributes vary from one period to another. Our setting also allows for sporadic deadline overruns and accounts for criticality during fault handling. A user interface was created to allow automatic generation of the models as well as visualization of the analysis results, whereas predictability is verified using the Spin model checker.

M3 - Article in proceedings

SP - 153

EP - 171

BT - Formal Aspects of Component Software

PB - Springer Link

ER -