Formal verification plays an important role in proving the safety of autonomous vehicles (AV). It is crucial to find errors in the AV system model to ensure safety critical features are not compromised. Model checking is a formal verification method which checks if the finite state machine (FSM) model meets system requirements. These requirements can be expressed as linear Temporal logic (LTL) formulae to describe a sequence of states with linear Temporal properties to be satisfied. NuSMV is a dedicated software for performing model checking based on Temporal logic formulae on FSM models. However, NuSMV does not provide model-based design. On the other hand, Stateflow in MATLAB/SIMULINK is a powerful tool for designing the model and offers an interactive Graphical User Interface (GUI) for the user/verifier but is not as efficient as NuSMV in model checking. Hence, model transformation becomes vital to convert the AV model in Stateflow to an input language of model checking software such as NuSMV. In this paper, we model an AV using Stateflow, which consists of cruise control, lane change/abortion, obstacle avoidance and gap maintenance blocks in the form of FSMs. We design an automatic verification tool to perform model transformation using a C compiler with NuSMV library included. Guard conditions are represented by Boolean expressions to capture the transition sequence between different blocks. LTL specifications of safety critical requirements are verified to guarantee the validity of the AV system design. When guard conditions fail, i.e., system requirements are not met, the verification tool will give a counterexample as the output. A case study is performed to show how this verification tool can help designers to make modifications based on the counterexamples to better meet the system requirements. We also perform a benchmark verification using the design verifier in SIMULINK to compare the performance. 1


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification of Autonomous Vehicles: Bridging the Gap between Model-Based Design and Model Checking


    Weitere Titelangaben:

    Sae Technical Papers


    Beteiligte:
    Rao, Ananya (Autor:in) / Wang, Yue (Autor:in)

    Kongress:

    WCX SAE World Congress Experience ; 2023



    Erscheinungsdatum :

    2023-04-11




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Model checking for autonomous vehicles

    FERGUSON DAVID I / DOLGOV DMITRI A / URMSON CHRISTOPHER | Europäisches Patentamt | 2016

    Freier Zugriff

    Trajectory Verification for Networked and Autonomous Vehicles using Temporal Logic and Model Checking

    Kloock, Maximilian / He, Qingyun / Kowalewski, Stefan et al. | IEEE | 2021


    Model-based Validation and Verification of Autonomous Networked Vehicles

    Sapronov, L. / Bose, P. / IEEE | British Library Conference Proceedings | 2005



    Towards Certification of Autonomous Unmanned Aircraft Using Formal Model Checking and Simulation

    Webster, Matt / Cameron, Neil / Jump, Michael et al. | AIAA | 2012