Resource-Parameterized Timing Analysis of Real-Time Systems

Publikation: Bidrag til bog/antologi/rapport/konference proceedingBidrag til bog/antologiForskningpeer review

3 Citationer (Scopus)

Resumé

Cyber-Physical Systems (CPS) are subject to platform-given resource constraints upon such resources as CPU, memory, and bus, in executing their functionalities. This causes the behavior of a verified application to deviate from its intended timing behavior when the application is integrated on a specic platform. For the same reason, a configuration of platforms cannot be independent from applications in most cases. This paper proposes a new analysis framework of real-time systems where an application and a platform can be analyzed in a fully independent way such that not only the application but also the platform once verfiied can be exploited by various applications. The dependent behaviors of application and platform are also analyzed by exploiting their individual models transformed from their independent models. To the end, we provide a highly configurable platform model that can be parameterized by various resource congurations. For analysis of application and platform models, we use two model checking techniques: symbolic and statistical model checking techniques of Uppaal. Our framework is demonstrated by a case study where a turn indicator system is analyzed with respect to various platform resource constraints.
OriginalsprogEngelsk
TitelHardware and Software: Verification and Testing : 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings
RedaktørerNir Piterman
ForlagSpringer
Publikationsdato2015
Sider190-205
ISBN (Trykt)978-3-319-26286-4
ISBN (Elektronisk) 978-3-319-26287-1
DOI
StatusUdgivet - 2015
BegivenhedInternational Haifa Verification Conference, HVC 2015 - Haifa, Israel
Varighed: 17 nov. 201519 nov. 2015
Konferencens nummer: 11th

Konference

KonferenceInternational Haifa Verification Conference, HVC 2015
Nummer11th
LandIsrael
ByHaifa
Periode17/11/201519/11/2015
NavnLecture Notes in Computer Science
Nummer9434
ISSN0302-9743

Citer dette

Kim, J. H., Legay, A., Larsen, K. G., Mikučionis, M., & Nielsen, B. (2015). Resource-Parameterized Timing Analysis of Real-Time Systems. I N. Piterman (red.), Hardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings (s. 190-205). Springer. Lecture Notes in Computer Science, Nr. 9434 https://doi.org/10.1007/978-3-319-26287-1_12
Kim, Jin Hyun ; Legay, Axel ; Larsen, Kim Guldstrand ; Mikučionis, Marius ; Nielsen, Brian. / Resource-Parameterized Timing Analysis of Real-Time Systems. Hardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings. red. / Nir Piterman. Springer, 2015. s. 190-205 (Lecture Notes in Computer Science; Nr. 9434).
@inbook{7aa5e037a63245a69fbeb8aff62fcb87,
title = "Resource-Parameterized Timing Analysis of Real-Time Systems",
abstract = "Cyber-Physical Systems (CPS) are subject to platform-given resource constraints upon such resources as CPU, memory, and bus, in executing their functionalities. This causes the behavior of a verified application to deviate from its intended timing behavior when the application is integrated on a specic platform. For the same reason, a configuration of platforms cannot be independent from applications in most cases. This paper proposes a new analysis framework of real-time systems where an application and a platform can be analyzed in a fully independent way such that not only the application but also the platform once verfiied can be exploited by various applications. The dependent behaviors of application and platform are also analyzed by exploiting their individual models transformed from their independent models. To the end, we provide a highly configurable platform model that can be parameterized by various resource congurations. For analysis of application and platform models, we use two model checking techniques: symbolic and statistical model checking techniques of Uppaal. Our framework is demonstrated by a case study where a turn indicator system is analyzed with respect to various platform resource constraints.",
author = "Kim, {Jin Hyun} and Axel Legay and Larsen, {Kim Guldstrand} and Marius Mikučionis and Brian Nielsen",
year = "2015",
doi = "10.1007/978-3-319-26287-1_12",
language = "English",
isbn = "978-3-319-26286-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "9434",
pages = "190--205",
editor = "Nir Piterman",
booktitle = "Hardware and Software: Verification and Testing",
address = "Germany",

}

Kim, JH, Legay, A, Larsen, KG, Mikučionis, M & Nielsen, B 2015, Resource-Parameterized Timing Analysis of Real-Time Systems. i N Piterman (red.), Hardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings. Springer, Lecture Notes in Computer Science, nr. 9434, s. 190-205, International Haifa Verification Conference, HVC 2015, Haifa, Israel, 17/11/2015. https://doi.org/10.1007/978-3-319-26287-1_12

Resource-Parameterized Timing Analysis of Real-Time Systems. / Kim, Jin Hyun ; Legay, Axel; Larsen, Kim Guldstrand; Mikučionis, Marius; Nielsen, Brian.

Hardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings. red. / Nir Piterman. Springer, 2015. s. 190-205 (Lecture Notes in Computer Science; Nr. 9434).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingBidrag til bog/antologiForskningpeer review

TY - CHAP

T1 - Resource-Parameterized Timing Analysis of Real-Time Systems

AU - Kim, Jin Hyun

AU - Legay, Axel

AU - Larsen, Kim Guldstrand

AU - Mikučionis, Marius

AU - Nielsen, Brian

PY - 2015

Y1 - 2015

N2 - Cyber-Physical Systems (CPS) are subject to platform-given resource constraints upon such resources as CPU, memory, and bus, in executing their functionalities. This causes the behavior of a verified application to deviate from its intended timing behavior when the application is integrated on a specic platform. For the same reason, a configuration of platforms cannot be independent from applications in most cases. This paper proposes a new analysis framework of real-time systems where an application and a platform can be analyzed in a fully independent way such that not only the application but also the platform once verfiied can be exploited by various applications. The dependent behaviors of application and platform are also analyzed by exploiting their individual models transformed from their independent models. To the end, we provide a highly configurable platform model that can be parameterized by various resource congurations. For analysis of application and platform models, we use two model checking techniques: symbolic and statistical model checking techniques of Uppaal. Our framework is demonstrated by a case study where a turn indicator system is analyzed with respect to various platform resource constraints.

AB - Cyber-Physical Systems (CPS) are subject to platform-given resource constraints upon such resources as CPU, memory, and bus, in executing their functionalities. This causes the behavior of a verified application to deviate from its intended timing behavior when the application is integrated on a specic platform. For the same reason, a configuration of platforms cannot be independent from applications in most cases. This paper proposes a new analysis framework of real-time systems where an application and a platform can be analyzed in a fully independent way such that not only the application but also the platform once verfiied can be exploited by various applications. The dependent behaviors of application and platform are also analyzed by exploiting their individual models transformed from their independent models. To the end, we provide a highly configurable platform model that can be parameterized by various resource congurations. For analysis of application and platform models, we use two model checking techniques: symbolic and statistical model checking techniques of Uppaal. Our framework is demonstrated by a case study where a turn indicator system is analyzed with respect to various platform resource constraints.

U2 - 10.1007/978-3-319-26287-1_12

DO - 10.1007/978-3-319-26287-1_12

M3 - Book chapter

SN - 978-3-319-26286-4

T3 - Lecture Notes in Computer Science

SP - 190

EP - 205

BT - Hardware and Software: Verification and Testing

A2 - Piterman, Nir

PB - Springer

ER -

Kim JH, Legay A, Larsen KG, Mikučionis M, Nielsen B. Resource-Parameterized Timing Analysis of Real-Time Systems. I Piterman N, red., Hardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings. Springer. 2015. s. 190-205. (Lecture Notes in Computer Science; Nr. 9434). https://doi.org/10.1007/978-3-319-26287-1_12