arXiv subjects

Bernd Westphal

Publications and source records attributed to Bernd Westphal.

6 recordsLinked to original sources

arXiv2025

Relevant HAL Interface Requirements for Embedded Systems

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.

cs.LO↗

arXiv2025

Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development

Temporal HAL-API Dependencies (THADs) can be useful to capture an interesting class of correctness properties in embedded software development. They demand a moderate effort for specification (which can be done via program annotations) and verification (which can be done automatically via software model checking). In this sense, they have the potential to form an interesting sweet spot between generic properties (that demand virtually no specification effort, and that are typically addressed by static analysis) and application-specific properties as addressed by full-fledged formal methods. Thus, they may form a gateway to wider and more economic use of formal methods in industrial embedded software development.

cs.SE↗

arXiv2025

Context-aware, Ante-hoc Explanations of Driving Behaviour

Autonomous vehicles (AVs) must be both safe and trustworthy to gain social acceptance and become a viable option for everyday public transportation. Explanations about the system behaviour can increase safety and trust in AVs. Unfortunately, explaining the system behaviour of AI-based driving functions is particularly challenging, as decision-making processes are often opaque. The field of Explainability Engineering tackles this challenge by developing explanation models at design time. These models are designed from system design artefacts and stakeholder needs to develop correct and good explanations. To support this field, we propose an approach that enables context-aware, ante-hoc explanations of (un)expectable driving manoeuvres at runtime. The visual yet formal language Traffic Sequence Charts is used to formalise explanation contexts, as well as corresponding (un)expectable driving manoeuvres. A dedicated runtime monitoring enables context-recognition and ante-hoc presentation of explanations at runtime. In combination, we aim to support the bridging of correct and good explanations. Our method is demonstrated in a simulated overtaking.

cs.LO↗

arXiv2025

Abstract Scene Graphs: Formalizing and Monitoring Spatial Properties of Automated Driving Functions

Automated Driving Functions (ADFs) need to comply with spatial properties of varied complexity while driving on public roads. Since such situations are safety-critical in nature, it is necessary to continuously check ADFs for compliance with their spatial properties. Due to their complexity, such spatial properties need to be formalized to enable their automated checking. Scene Graphs (SGs) allow for an explicit structured representation of objects present in a traffic scene and their spatial relationships to each other. In this paper, we build upon the SG construct and propose the Abstract Scene Graph (ASG) formalism to formalize spatial properties of ADFs. We show using real-world examples how spatial properties can be formalized using ASGs. Finally, we present a framework that uses ASGs to perform Runtime Monitoring of ADFs. To this end, we also show algorithmically how a spatial property formalized as an ASG can be satisfied by ADF system behaviour.

cs.LO↗

arXiv2023

IMoG -- a methodology for modeling future microelectronic innovations

[Context and motivation] The automotive industry is currently undergoing a fundamental transformation towards software defined vehicles. The automotive market of the future demands a higher level of automation, electrification of the power train, and individually configurable comfort functions. [Question/problem] These demands pose a challenge to the automotive development cycle, because they introduce complexity by larger and not yet well explored design spaces that are difficult to manage. [Principal ideas/results] To cope with these challenges, the main players along the value chain have an increased interest in collaborating and aligning their development efforts along joint roadmaps. Roadmap development can be viewed as a field of requirements engineering with the goal to capture product aspects on an appropriate level of abstraction to speed up investment decisions, reduce communication overhead and parallelize development activities, while complying with competition laws. [Contribution] In this paper, we present a refinement of the "Innovation Modeling Grid" (IMoG), which encompasses a methodology, a process and a proposed notation to support joint analysis of development roadmaps. IMoG is focused on the automotive domain, yet there are clear potentials for other applications.

cs.SI↗

arXiv2022

Towards Runtime Monitoring of Complex System Requirements for Autonomous Driving Functions

Autonomous driving functions (ADFs) in public traffic have to comply with complex system requirements that are based on knowledge of experts from different disciplines, e.g., lawyers, safety experts, psychologists. In this paper, we present a research preview regarding the validation of ADFs with respect to such requirements. We investigate the suitability of Traffic Sequence Charts (TSCs) for the formalization of such requirements and present a concept for monitoring system compliance during validation runs. We find TSCs, with their intuitive visual syntax over symbols from the traffic domain, to be a promising choice for the collaborative formalization of such requirements. For an example TSC, we describe the construction of a runtime monitor according to our novel concept that exploits the separation of spatial and temporal aspects in TSCs, and successfully apply the monitor on exemplary runs. The monitor continuously provides verdicts at runtime, which is particularly beneficial in ADF validation, where validation runs are expensive. The next open research questions concern the generalization of our monitor construction, the identification of the limits of TSC monitorability, and the investigation of the monitor's performance in practical applications. Perspectively, TSC runtime monitoring could provide a useful technique in other emerging application areas such as AI training, safeguarding ADFs during operation, and gathering meaningful traffic data in the field.

cs.LO↗