Model-Based Formal Verification and Hybrid Fault-Tolerance for Safety-Critical Autonomous Vehicle Systems

ABSTRACT: Reliability and safety assurance in autonomous vehicle systems and related cyber-physical systems (CPSs) deployed in life-critical domains—such as automotive safety, avionics, industrial automation, and transportation—require rigorous verification and validation (V&V). Design errors in system specifications and hardware/software (HW/SW) faults within architectural models can compromise functionality and lead to catastrophic outcomes. This paper introduces a model-based verification framework that integrates formal verification with hybrid fault-tolerance mechanisms, demonstrated through a safety-critical Seatbelt Reminder (SBR) subsystem as part of intelligent vehicle safety architectures. The proposed design employs Simulink Design Verifier (SLDV) as a formal model checker to validate safety properties, while an embedded Triple Modular Redundancy (TMR) scheme detects and masks both transient and permanent faults. Simulation results show that safety property proofs were achieved with preprocessing and analysis times of 10 and 12 s, respectively. Runtime execution of the verifiable model demonstrated high dependability across diverse safety-critical properties, and the TMR system meets high reliability equal to 99.3096 × 10⁻² with a failure rate of 0.005 failure per hour. Validation on a processor operating at 1500 MHz with 16 GB memory confirmed the effectiveness of the approach in enhancing reliability, fault resilience, and overall dependability in autonomous vehicle CPS design.