The 7th International Workshop on Automotive System/Software Architectures (WASA 2021) was collocated with the 18th International Conference on Software Architecture (ICSA 2021). During the WASA workshop, our colleagues presented the paper Architecture-based Hybrid Approach to Verify Safety-critical Automotive System Functions by Combining Data-driven and Formal Methods.
Due to the COVID-19 pandameic, both the ICSA conference and the WASA workshop were organized as virtual events.
Safety-critical automotive functions are required to satisfy stringent safety requirements. To guarantee the safety of such functions, their conformance with industry approved standards as well as statutory regulations must be ensured. Testing is the main method for checking automotive system functions, yet testing is incomplete and cannot show correctness. Inherent uncertainties in the physical environment introduce non-determinism in testing, increasing the difficulty of replicating environmental stimuli relevant for edge cases, and thus, the effort invested in road tests to produce statistical significance. Formal verification techniques are able to show correctness and are recommended for functions with higher automotive safety integrity levels (ASIL), e.g. for ASIL D. However, formal verification has scalability issues in case of highly complex automotive systems and heterogeneous sensor data received as inputs. To address these challenges, this paper proposes a novel architecture-based approach which combines data-driven methods with formal methods for the verification of safety-critical automotive functions, with consideration of the system decomposition within the functional system architecture. We illustrate the application of our concept on two industrial automotive functions, speed estimation and exhaust aftertreatment, and report on results and lessons learned.