Search Results

The software architecture behind modern autonomous vehicles (AV) is becoming more complex steadily. Safety verification is now an imminent task prior to the large-scale deployment of such convoluted models. For safety-critical tasks in navigation, it becomes imperative to perform a verification procedure on the trajectories proposed by the planning algorithm prior to deployment. Signal Temporal Logic (STL) constraints can dictate the safety requirements for an AV. A combination of STL constraints is called a specification. A key difference between STL and other logic constraints is that STL allows us to work on continuous signals. We verify the satisfaction of the STL specifications by calculating the robustness value for each signal within the specification. Higher robustness values indicate a safer system. Model Predictive Control (MPC) is one of the most widely used methods to control the navigation of an AV, with an underlying set of state and input constraints.

In the United States and worldwide, 38,824 and 1.35 million people were killed in vehicle crashes during 2020. These statistics are tragic and indicative of an on-going public health crisis centered on automobiles and other ground transportation solutions. Although the long-term US vehicle fatality rate is slowly declining, it continues to be elevated compared to European countries. The introduction of vehicle safety systems and re-designed roadways has improved survivability and driving environment, but driver behavior has not been fully addressed. A non-confrontational approach is the evaluation of driver behavior using onboard sensors and computer algorithms to determine the vehicle’s “mistrust” level of the given operator and the safety of the individual operating the vehicle. This is an inversion of the classic human-machine trust paradigm in which the human evaluates whether the machine can safely operate in an automated fashion.

Vehicular control systems are characterized with numerous complex interactions with a steady rise of autonomous functions, which makes it more challenging for designers and safety engineers to identify unexpected failures. These systems tend to be highly integrated and exhibit features like concurrency for which traditional verification and validation techniques (i.e. testing and simulation) are insufficient to provide rigorous and complete assessment. Model Checking, a well-known formal verification technique, can be used to rigorously prove the correctness of such systems according to design Requirements. In particular, Model Checking is a method for formally verifying finite-state concurrent systems. Specifications about the system are expressed as temporal logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not.

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.