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.

翻译：嵌入式应用常通过硬件抽象层（HAL）访问硬件。对HAL的不当使用可能导致硬件操作错误，引发系统故障甚至对硬件造成严重损害。问题在于如何从可能庞大的HAL接口需求集中，优先识别出那些对预防此类系统故障具有明确相关性的需求。本文提出一种形式化的相关性定义，使我们能够借助形式化方法（即软件模型检验）生成数学证明，确认某项需求具有无可争议的相关性。我们提出一种从系统故障问题报告中提取可证明相关需求的方法，并通过案例研究论证该方法的理论可行性。案例研究基于三个使用spidev HAL通过SPI总线的嵌入式应用问题报告实例。本文的核心贡献在于为研究新型需求优先级排序方法开辟了道路，该方法专门针对预防特定类型的系统故障。