Building a Digital Thread Platform to Enable Bidirectional Design Convergence between Upstream Requirements and Downstream Specifications via MBSE

SEISHI SHIMAMURA･HARUHISA TSUCHIKAWA･CHISATO SUZUKI･ASAMI HOZUMI･KIYOTAKA SHOJI･RYUZO NOGUCHI･SO NISIHWAKI･RYOJI KATSUKI (Nissan Motor)

This paper reports a digital-thread platform aligned with MBSE that bidirectionally links requirements and component specifications via physics-based models. With SPDM-based unified management and event-driven automated handoffs, it advances automation from requirement updates through analysis/optimization to design finalization and registration. Internal projects showed shorter change-to-result lead time and improved traceability.

Selection of model development guidelines for MBD development system

SEUNGJUN BACK (hyundai motor)

MBD (Model Design Development) is investigated for applying to develop automotive controller. In order to implement MBD in automotive, the development guideline is indispensable. When compared with investigation of the guideline such as MISRA C in C-code, however, the investigation on MBD is currently insufficient. In this paper, we studied the selection of guidelines for the development of MBD of the thermal energy system controller. Comparing MISRA AC SLSF:2023 and MAB 5.0, we selected and applied the guidelines for the development of the thermal energy system controller. Design of data precision is presented for actuator control.

Sound Static Analysis for Safety and Security

Daniel Kaestner･Ferdinand Christian (AbsInt GmbH)

Runtime errors such as buffer overflows or data races are safety- and security-relevant code defects. A sound static analyzer reports all such defects in the code, can prove their absence, and covers further verification objectives such as code guideline checking as well as data and control flow analysis. The analysis can be used to satisfy requirements from norms like ISO 26262, ISO 21434, and from the novel European Cyber Resilience Act (CRA). We will show practical experiments that demonstrate that sound static analysis scales for real-life AUTOSAR integration projects.

Formally Verified Compilation in the Context of Functional Safety

Daniel Kaestner･Adrian Dapprich･Alexander Rogovskyy (AbsInt GmbH)

CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. This presentation gives an overview of design and proof concept of CompCert, and gives experimental data about performance and size of the generated code on TriCore Aurix. We describe novel contributions to improve the efficiency of the software development and verification process, and discuss the tool qualification strategy with respect to current safety norms.

Model Checking of Automotive Software with CBMC

Shinya Miharu･Wenhung Huang (DENSO)

As automotive software becomes larger and more complex, bugs that are difficult to detect with existing verification processes are increasing. This study focuses on model checking and proposes a method for applying it to the verification process of automotive software. Furthermore, we report the results of evaluating its applicability using internal case studies, as well as future prospects.

Why Model Credibility Is not Enough: Rethinking Trust in Simulation Architectures

Romain Barbedienne･Boussaad Soualmi･Adeline Lanugue (IRT SystemX)･Julien Silande (Keysight)･Anthony Levillain (OPmobility)･Cedric Leclerc (Renault Group)･Maxime Hayet (Stellantis)･Rim Kaddah･Cristian Maxim (IRT SystemX)

Assessing the credibility of simulation models is crucial, yet models are often integrated within broader simulation architectures. Can the credibility of simulation architectures be derived from their constituent models? This paper explores this question by reviewing state-of-the-art approaches in assembly credibility, including sensitivity analysis, expert qualitative analysis, AI explainability, and network-based methods. Each approach is evaluated according to "rigor", "generalizability", and "resource requirements", highlighting their respective strengths and limitations. The analysis provides insights into the feasibility and challenges of assessing architectural credibility, offering a foundation for future research in this emerging field.