Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Relevant HAL Interface Requirements for Embedded Systems

Manuel Bentele, Andreas Podelski, Axel Sikora, Bernd Westphal

TL;DR

The paper tackles the problem of prioritizing HAL interface requirements to prevent hardware-damaging failures by introducing a formal relevance criterion. It proposes two workflows—extract-and-check a single candidate from failure reports and bulk-check a candidate set using formal verification—to prove that a requirement is indisputably relevant. A SPI/spidev case study demonstrates feasibility: three temporal dependencies among 26 candidates are proven relevant, guiding developers to focus on critical HAL usage. The work provides a principled, verifiable approach to hal interface requirements that can improve reliability in embedded software and prevent specific failure modes.

Abstract

Embedded applications often use a Hardware Abstraction Layer (HAL) to access hardware. Improper use of the HAL can lead to incorrect hardware operations, resulting in system failure and potentially serious damage to the hardware. The question is how one can obtain prioritize, among a possibly large set of HAL interface requirements, those that are indisputably relevant for preventing this kind of system failure. In this paper, we introduce a formal notion of relevance. This allows us to leverage a formal method, i.e., software model checking, to produce a mathematical proof that a requirement is indisputably relevant. We propose an approach to extract provably relevant requirements from issue reports on system failures. We present a case study to demonstrate that the approach is feasible in principle. The case study uses three examples of issue reports on embedded applications that use the SPI bus via the spidev HAL. The overall contribution of this paper is to pave the way for the study of approaches to a new kind of prioritization aimed at preventing a specific kind of system failure.

Relevant HAL Interface Requirements for Embedded Systems

TL;DR

The paper tackles the problem of prioritizing HAL interface requirements to prevent hardware-damaging failures by introducing a formal relevance criterion. It proposes two workflows—extract-and-check a single candidate from failure reports and bulk-check a candidate set using formal verification—to prove that a requirement is indisputably relevant. A SPI/spidev case study demonstrates feasibility: three temporal dependencies among 26 candidates are proven relevant, guiding developers to focus on critical HAL usage. The work provides a principled, verifiable approach to hal interface requirements that can improve reliability in embedded software and prevent specific failure modes.

Abstract

Embedded applications often use a Hardware Abstraction Layer (HAL) to access hardware. Improper use of the HAL can lead to incorrect hardware operations, resulting in system failure and potentially serious damage to the hardware. The question is how one can obtain prioritize, among a possibly large set of HAL interface requirements, those that are indisputably relevant for preventing this kind of system failure. In this paper, we introduce a formal notion of relevance. This allows us to leverage a formal method, i.e., software model checking, to produce a mathematical proof that a requirement is indisputably relevant. We propose an approach to extract provably relevant requirements from issue reports on system failures. We present a case study to demonstrate that the approach is feasible in principle. The case study uses three examples of issue reports on embedded applications that use the SPI bus via the spidev HAL. The overall contribution of this paper is to pave the way for the study of approaches to a new kind of prioritization aimed at preventing a specific kind of system failure.

Paper Structure

This paper contains 33 sections, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. An approach based on relevance
  3. Notion of relevance
  4. Extract and check a single candidate requirement for relevance
  5. Extract candidate from issue report.
  6. Inspect issue report.
  7. Extract candidate requirement.
  8. Check relevance of extracted candidate.
  9. First decision of relevance check.
  10. Second decision of relevance check.
  11. Check a set of candidate requirements for relevance
  12. Case study
  13. System failures in embedded systems
  14. Overview of systems.
  15. spi bus and spidev hal.
  16. ...and 18 more sections

Figures (3)

  • Figure 1: Overall approach. The application code comes in two versions: the original version exhibits the system failure, the repaired version does not.
  • Figure 2: Alternative approach. The finite set of candidate requirements $\mathcal{R}$ is fixed for a given hal interface. The application code comes again in two versions: the original version exhibits the system failure, the repaired version does not.
  • Figure 3: Architecture of the embedded system from the issue report in RaspberryPiForum2019.

Theorems & Definitions (1)

  • definition thmcounterdefinition: Relevance