Formal Verification of Safety-Critical Control Flow in Distributed Embedded Systems Using Model Checking and Symbolic Executions

Abstract

Ensuring the correctness of control flow in distributed embedded systems is vital, particularly in safety-critical domains like automotive, aerospace, and industrial automation. Traditional testing is often insufficient due to the system’s distributed nature and real-time constraints. This paper proposes a hybrid approach that combines model checking and symbolic execution to verify the safety properties of distributed control flows. We analyze control flow correctness, deadlock-freedom, and reachability through formal methods applied to a representative system architecture. Our findings demonstrate that the integrated approach can reveal latent faults undetected by conventional testing and simulation-based techniques. Experimental results validate the efficacy of this method in detecting critical errors with acceptable computational overhead.