7.7 Rigorous design, analysis, and monitoring of dependable embedded systems

Time	Label	Presentation Title Authors
14:30	7.7.1	CHASE: CONTRACT-BASED REQUIREMENT ENGINEERING FOR CYBER-PHYSICAL SYSTEM DESIGN Speaker: Pierluigi Nuzzo, University of Southern California, US Authors: Pierluigi Nuzzo¹, Michele Lora², Yishai Feldman³ and Alberto Sangiovanni-Vincentelli⁴ ¹University of Southern California, US; ²University of Verona, IT; ³IBM Research, Haifa, IL; ⁴University of California at Berkeley, US Abstract This paper presents CHASE, a framework for requirement capture, formalization, and validation for cyber-physical systems. CHASE combines a practical front-end formal specification language based on patterns with a rigorous verification back-end based on assume-guarantee contracts. The front-end language can express temporal properties of networks using a declarative style, and supports automatic translation from natural-language constructs to low-level mathematical languages. The verification back-end leverages the mathematical formalism of contracts to reason about system requirements and determine inconsistencies and dependencies between them. CHASE features a modular and extensible software infrastructure that can support different domain-specific languages, modeling formalisms, and analysis tools. We illustrate its effectiveness on industrial design examples, including control of aircraft power distribution networks and arbitration of a mixed-criticality automotive bus. Download Paper (PDF; Only available from the DATE venue WiFi)
15:00	7.7.2	RESILIENCE EVALUATION VIA SYMBOLIC FAULT INJECTION ON INTERMEDIATE CODE Speaker: Hoang M. Le, University of Bremen, DE Authors: Hoang M. Le¹, Vladimir Herdt¹, Daniel Grosse² and Rolf Drechsler² ¹University of Bremen, DE; ²University of Bremen/DFKI GmbH, DE Abstract There is a growing need for error-resilient software that can tolerate hardware faults as well as for new resilience evaluation techniques. For the latter, a promising direction is to apply formal techniques in fault injection-based evaluations to improve the coverage of evaluation results. Building on the recent development of Software-implemented Fault Injection (SWiFI) techniques on compiler's intermediate code, this paper proposes a novel resilience evaluation framework combining LLVM-based SWiFI and SMT-based symbolic execution. This novel combination offers significant advantages over state-of-the-art approaches with respect to accuracy and coverage. Download Paper (PDF; Only available from the DATE venue WiFi)
15:30	7.7.3	ONLINE ANALYSIS OF DEBUG TRACE DATA FOR EMBEDDED SYSTEMS Speaker: Philip Gottschling, TU Darmstadt, DE Authors: Normann Decker¹, Boris Dreyer², Philip Gottschling², Christian Hochberger², Alexander Lange³, Martin Leucker¹, Torben Scheffel¹, Simon Wegener⁴ and Alexander Weiss³ ¹Universität zu Lübeck, DE; ²TU Darmstadt, DE; ³Accemic Technologies GmbH, DE; ⁴AbsInt Angewandte Informatik GmbH, DE Abstract Modern multi-core Systems-on-Chip (SoC) provide very high computational power. On the downside, they are hard to debug and it is often very difficult to understand what is going on in these chips because of the limited observability inside the SoC. Chip manufacturers try to compensate this difficulty by providing highly compressed trace data from the individual cores. In the past, the common way to deal with this data was storing it for later offline analysis, which severely limits the time span that can be observed. In this contribution, we present an FPGA-based solution that is able to process the trace data in real-time, enabling continuous observation of the state of a core. Moreover, we discuss applications enabled by this technology. Download Paper (PDF; Only available from the DATE venue WiFi)
16:00		End of session Coffee Break in Exhibition Area Coffee Breaks in the Exhibition Area On all conference days (Tuesday to Thursday), coffee and tea will be served during the coffee breaks at the below-mentioned times in the exhibition area (Terrace Level of the ICCD). Lunch Breaks (Großer Saal + Saal 1) On all conference days (Tuesday to Thursday), a seated lunch (lunch buffet) will be offered in the rooms "Großer Saal" and "Saal 1" (Saal Level of the ICCD) to fully registered conference delegates only. There will be badge control at the entrance to the lunch break area. Tuesday, March 20, 2018 Coffee Break 10:30 - 11:30 Lunch Break 13:00 - 14:30 Awards Presentation and Keynote Lecture in "Saal 2" 13:50 - 14:20 Coffee Break 16:00 - 17:00 Wednesday, March 21, 2018 Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:30 Awards Presentation and Keynote Lecture in "Saal 2" 13:30 - 14:20 Coffee Break 16:00 - 17:00 Thursday, March 22, 2018 Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:00 Keynote Lecture in "Saal 2" 13:20 - 13:50 Coffee Break 15:30 - 16:00

Time

Label

Presentation Title
Authors

14:30

7.7.1

CHASE: CONTRACT-BASED REQUIREMENT ENGINEERING FOR CYBER-PHYSICAL SYSTEM DESIGN
Speaker:
Pierluigi Nuzzo, University of Southern California, US
Authors:
Pierluigi Nuzzo¹, Michele Lora², Yishai Feldman³ and Alberto Sangiovanni-Vincentelli⁴
¹University of Southern California, US; ²University of Verona, IT; ³IBM Research, Haifa, IL; ⁴University of California at Berkeley, US
Abstract
This paper presents CHASE, a framework for requirement capture, formalization, and validation for cyber-physical systems. CHASE combines a practical front-end formal specification language based on patterns with a rigorous verification back-end based on assume-guarantee contracts. The front-end language can express temporal properties of networks using a declarative style, and supports automatic translation from natural-language constructs to low-level mathematical languages. The verification back-end leverages the mathematical formalism of contracts to reason about system requirements and determine inconsistencies and dependencies between them. CHASE features a modular and extensible software infrastructure that can support different domain-specific languages, modeling formalisms, and analysis tools. We illustrate its effectiveness on industrial design examples, including control of aircraft power distribution networks and arbitration of a mixed-criticality automotive bus.
Download Paper (PDF; Only available from the DATE venue WiFi)

15:00

7.7.2

RESILIENCE EVALUATION VIA SYMBOLIC FAULT INJECTION ON INTERMEDIATE CODE
Speaker:
Hoang M. Le, University of Bremen, DE
Authors:
Hoang M. Le¹, Vladimir Herdt¹, Daniel Grosse² and Rolf Drechsler²
¹University of Bremen, DE; ²University of Bremen/DFKI GmbH, DE
Abstract
There is a growing need for error-resilient software that can tolerate hardware faults as well as for new resilience evaluation techniques. For the latter, a promising direction is to apply formal techniques in fault injection-based evaluations to improve the coverage of evaluation results. Building on the recent development of Software-implemented Fault Injection (SWiFI) techniques on compiler's intermediate code, this paper proposes a novel resilience evaluation framework combining LLVM-based SWiFI and SMT-based symbolic execution. This novel combination offers significant advantages over state-of-the-art approaches with respect to accuracy and coverage.
Download Paper (PDF; Only available from the DATE venue WiFi)

15:30

7.7.3

ONLINE ANALYSIS OF DEBUG TRACE DATA FOR EMBEDDED SYSTEMS
Speaker:
Philip Gottschling, TU Darmstadt, DE
Authors:
Normann Decker¹, Boris Dreyer², Philip Gottschling², Christian Hochberger², Alexander Lange³, Martin Leucker¹, Torben Scheffel¹, Simon Wegener⁴ and Alexander Weiss³
¹Universität zu Lübeck, DE; ²TU Darmstadt, DE; ³Accemic Technologies GmbH, DE; ⁴AbsInt Angewandte Informatik GmbH, DE
Abstract
Modern multi-core Systems-on-Chip (SoC) provide very high computational power. On the downside, they are hard to debug and it is often very difficult to understand what is going on in these chips because of the limited observability inside the SoC. Chip manufacturers try to compensate this difficulty by providing highly compressed trace data from the individual cores. In the past, the common way to deal with this data was storing it for later offline analysis, which severely limits the time span that can be observed. In this contribution, we present an FPGA-based solution that is able to process the trace data in real-time, enabling continuous observation of the state of a core. Moreover, we discuss applications enabled by this technology.
Download Paper (PDF; Only available from the DATE venue WiFi)

16:00

End of session
Coffee Break in Exhibition Area

Coffee Breaks in the Exhibition Area

On all conference days (Tuesday to Thursday), coffee and tea will be served during the coffee breaks at the below-mentioned times in the exhibition area (Terrace Level of the ICCD).

Lunch Breaks (Großer Saal + Saal 1)

On all conference days (Tuesday to Thursday), a seated lunch (lunch buffet) will be offered in the rooms "Großer Saal" and "Saal 1" (Saal Level of the ICCD) to fully registered conference delegates only. There will be badge control at the entrance to the lunch break area.

Tuesday, March 20, 2018