Checking the HAL Interface Specification Continuously, Right from the Start

TL;DR

This paper introduces a novel method for continuously verifying HAL interface specifications during embedded application development, leveraging software model checking to ensure correctness from the initial skeleton to the final program.

Contribution

It presents a new approach that applies software model checking iteratively during development, enabling early detection of interface specification errors without formal step connections.

Findings

Check succeeds at each development step

Approach is promising based on preliminary evaluation

Ensures correct HAL interface usage from start to finish

Abstract

The correct use of a Hardware Abstraction Layer (HAL) interface in embedded applications is crucial to prevent malfunctions, crashes, or even hardware damage. Software model checking has been successfully applied to check interface specifications in application programs, but its employment in industrial practice is hindered by its unpredictability (whether it succeeds for a given application program or not). In this paper, we present a novel approach to address this problem by checking the HAL interface specification continuously and right from the start of the development. I.e., we develop an embedded application in several iterations without a formal connection between the steps. The steps start from a program skeleton which does nothing but calling HAL functions. Actual functionality is added consecutively. The HAL interface specification is checked in each step of the sequence. The idea of the approach is to exploit a specific feature of software model checking: Its attempt to compute exactly the abstraction that is needed for the check to succeed may carry over from one step to the next, even if there is no formal connection between the steps. The experience from a preliminary experimental evaluation of our approach in the development of embedded applications is very promising. Following our approach, the check succeeds in each step and in particular in the final application program.