Checking the HAL Interface Specification Continuously, Right from the Start
Manuel Bentele, Onur Altinordu, Jan K\"orner, Andreas Podelski, Axel Sikora

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Security and Verification in Computing
