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 proceedingArticle in proceedingsResearchpeer-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 languageEnglish
Title of host publicationCyber Physical Systems. Model-Based Design
EditorsRoger Chamberlain, Martin Edin Grimheden, Walid Taha
Place of PublicationCham
PublisherSpringer
Publication date1 Jan 2020
Pages203-227
ISBN (Print)978-3-030-41130-5
DOIs
Publication statusPublished - 1 Jan 2020
Event9th 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 201918 Oct 2019

Conference

Conference9th 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
CountryUnited States
CityNew York City
Period17/10/201918/10/2019
SeriesLecture Notes in Computer Science
Volume11971
ISSN0302-9743

Keywords

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

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