Towards Formal Co-validation of Hardware and Software Timing Models of CPSs

Mihail Asavoae; Imane Haur; Mathieu Jan; Belgacem Ben Hedia; Martin Schoeberl

doi:10.1007/978-3-030-41131-2_10

Towards Formal Co-validation of Hardware and Software Timing Models of CPSs

Mihail Asavoae, Imane Haur, Mathieu Jan^*, Belgacem Ben Hedia, Martin Schoeberl

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

34 Downloads (Pure)

Abstract

Timing analysis of safety-critical systems derives timing bounds of applications, or software (SW), executed on dedicated platforms, or hardware (HW). The ensemble HW–SW features, from a timing perspective, two different types of computation – a SW-specific, instruction-driven timing progression and a HW-specific, cycle-driven one. The two timings are unified under a concept of timing model, which is crucial to establish a sound and precise worst-case timing reasoning. In this paper, we propose an investigation on how to systematically derive and formally prove such timing models. Our approach is exemplified on a simple, accumulator-based processor called Lipsi.

Original language	English
Title of host publication	Cyber Physical Systems. Model-Based Design
Editors	Roger Chamberlain, Martin Edin Grimheden, Walid Taha
Place of Publication	Cham
Publisher	Springer
Publication date	1 Jan 2020
Pages	203-227
ISBN (Print)	978-3-030-41130-5
DOIs	https://doi.org/10.1007/978-3-030-41131-2_10
Publication status	Published - 1 Jan 2020
Event	9th International Workshop on Model-Based Design of Cyber Physical Systems, CyPhy 2019 and 15th International Workshop on Embedded and Cyber-Physical Systems Education, WESE 2019, held in conjunction with ESWeek 2019 - New York City, United States Duration: 17 Oct 2019 → 18 Oct 2019

Conference

Conference	9th International Workshop on Model-Based Design of Cyber Physical Systems, CyPhy 2019 and 15th International Workshop on Embedded and Cyber-Physical Systems Education, WESE 2019, held in conjunction with ESWeek 2019
Country	United States
City	New York City
Period	17/10/2019 → 18/10/2019

Series	Lecture Notes in Computer Science
Volume	11971
ISSN	0302-9743

Keywords

Timing analysis
Timing model
Formal semantics
Chisel
HW/SW co-validation

Access to Document

10.1007/978-3-030-41131-2_10

FulltextAccepted author manuscript, 340 KB

Cite this

Asavoae, M., Haur, I., Jan, M., Ben Hedia, B., & Schoeberl, M. (2020). Towards Formal Co-validation of Hardware and Software Timing Models of CPSs. In R. Chamberlain, M. Edin Grimheden, & W. Taha (Eds.), Cyber Physical Systems. Model-Based Design (pp. 203-227). Springer. Lecture Notes in Computer Science, Vol.. 11971 https://doi.org/10.1007/978-3-030-41131-2_10

@inproceedings{88312aae16a3456a82b96b458af9476a,

title = "Towards Formal Co-validation of Hardware and Software Timing Models of CPSs",

abstract = "Timing analysis of safety-critical systems derives timing bounds of applications, or software (SW), executed on dedicated platforms, or hardware (HW). The ensemble HW–SW features, from a timing perspective, two different types of computation – a SW-specific, instruction-driven timing progression and a HW-specific, cycle-driven one. The two timings are unified under a concept of timing model, which is crucial to establish a sound and precise worst-case timing reasoning. In this paper, we propose an investigation on how to systematically derive and formally prove such timing models. Our approach is exemplified on a simple, accumulator-based processor called Lipsi.",

keywords = "Timing analysis, Timing model, Formal semantics, Chisel, HW/SW co-validation",

author = "Mihail Asavoae and Imane Haur and Mathieu Jan and {Ben Hedia}, Belgacem and Martin Schoeberl",

year = "2020",

month = jan

day = "1",

doi = "10.1007/978-3-030-41131-2_10",

language = "English",

isbn = "978-3-030-41130-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "203--227",

editor = "Roger Chamberlain and {Edin Grimheden}, Martin and Walid Taha",

booktitle = "Cyber Physical Systems. Model-Based Design",

note = "9th International Workshop on Model-Based Design of Cyber Physical Systems, CyPhy 2019 and 15th International Workshop on Embedded and Cyber-Physical Systems Education, WESE 2019, held in conjunction with ESWeek 2019 ; Conference date: 17-10-2019 Through 18-10-2019",

}

Asavoae, M, Haur, I, Jan, M, Ben Hedia, B & Schoeberl, M 2020, Towards Formal Co-validation of Hardware and Software Timing Models of CPSs. in R Chamberlain, M Edin Grimheden & W Taha (eds), Cyber Physical Systems. Model-Based Design . Springer, Cham, Lecture Notes in Computer Science, vol. 11971, pp. 203-227, 9th International Workshop on Model-Based Design of Cyber Physical Systems, CyPhy 2019 and 15th International Workshop on Embedded and Cyber-Physical Systems Education, WESE 2019, held in conjunction with ESWeek 2019, New York City, United States, 17/10/2019. https://doi.org/10.1007/978-3-030-41131-2_10

Towards Formal Co-validation of Hardware and Software Timing Models of CPSs. / Asavoae, Mihail; Haur, Imane; Jan, Mathieu; Ben Hedia, Belgacem; Schoeberl, Martin.

Cyber Physical Systems. Model-Based Design . ed. / Roger Chamberlain; Martin Edin Grimheden; Walid Taha. Cham : Springer, 2020. p. 203-227 (Lecture Notes in Computer Science, Vol. 11971).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Towards Formal Co-validation of Hardware and Software Timing Models of CPSs

AU - Asavoae, Mihail

AU - Haur, Imane

AU - Jan, Mathieu

AU - Ben Hedia, Belgacem

AU - Schoeberl, Martin

PY - 2020/1/1

Y1 - 2020/1/1

N2 - Timing analysis of safety-critical systems derives timing bounds of applications, or software (SW), executed on dedicated platforms, or hardware (HW). The ensemble HW–SW features, from a timing perspective, two different types of computation – a SW-specific, instruction-driven timing progression and a HW-specific, cycle-driven one. The two timings are unified under a concept of timing model, which is crucial to establish a sound and precise worst-case timing reasoning. In this paper, we propose an investigation on how to systematically derive and formally prove such timing models. Our approach is exemplified on a simple, accumulator-based processor called Lipsi.

AB - Timing analysis of safety-critical systems derives timing bounds of applications, or software (SW), executed on dedicated platforms, or hardware (HW). The ensemble HW–SW features, from a timing perspective, two different types of computation – a SW-specific, instruction-driven timing progression and a HW-specific, cycle-driven one. The two timings are unified under a concept of timing model, which is crucial to establish a sound and precise worst-case timing reasoning. In this paper, we propose an investigation on how to systematically derive and formally prove such timing models. Our approach is exemplified on a simple, accumulator-based processor called Lipsi.

KW - Timing analysis

KW - Timing model

KW - Formal semantics

KW - Chisel

KW - HW/SW co-validation

U2 - 10.1007/978-3-030-41131-2_10

DO - 10.1007/978-3-030-41131-2_10

M3 - Article in proceedings

AN - SCOPUS:85081173568

SN - 978-3-030-41130-5

T3 - Lecture Notes in Computer Science

SP - 203

EP - 227

BT - Cyber Physical Systems. Model-Based Design

A2 - Chamberlain, Roger

A2 - Edin Grimheden, Martin

A2 - Taha, Walid

PB - Springer

CY - Cham

T2 - 9th International Workshop on Model-Based Design of Cyber Physical Systems, CyPhy 2019 and 15th International Workshop on Embedded and Cyber-Physical Systems Education, WESE 2019, held in conjunction with ESWeek 2019

Y2 - 17 October 2019 through 18 October 2019

ER -