Introduction of driver's delay into 'model checking' for verification of safe interactions between a driver and an automated driving system

This study introduces the behavior of human driver's delay in model checking to verify the interaction between a driver and an automated driving system (ADS). An ADS interacts with humans, including other drivers and pedestrians to ensure safety on roads. In particular, human drivers and Level 3 ADSs must take control of the vehicle when the safety may be compromised. Since human driver behavior is sometimes unpredictable, it may cause accidents with other automated vehicles which are on the same roads even though automated vehicles have been introduced to decrease accidents. Hence, the interaction of automated vehicles with human drivers and their behavior should be taken into consideration to better understand when the interactions might fail. We make a model using communicating sequential processes (CSP) to analyze those interactions based on the architecture of the system of systems related to automated vehicles with SysML (Systems Modeling Language). By using CSP that is used to analyze processes of a concurrent system, interactions among the ADS and the driver behavior concurrently during driving can be learned. Wait processes and atomic processes on CSP are utilized to express the driver's processes with delay or without any delay. We demonstrate that the CSP model can express the driver's delay and model checking can verify the interactions among the ADS and the driver behavior.