Latest revision as of 20:09, 1 February 2021

Abstract

Research into safety in autonomous and semi-autonomous vehicles has, so far, largely been focused on testing and validation through simulation. Due to the fact that failure of these autonomous systems is potentially life-endangering, formal methods arise as a complementary approach. This paper studies the application of formal methods to the verification of a human driver model built using the cognitive architecture ACT-R, and to the design of correct-by-construction Advanced Driver Assistance Systems (ADAS). The novelty lies in the integration of ACT-R in the formal analysis and an abstraction technique that enables finite representation of a large dimensional, continuous system in the form of a Markov process. The situation considered is a multi-lane highway driving scenario and the interactions that arise. The efficacy of the method is illustrated in two case studies with various driving conditions.

Comment: Proceedings at IEEE CAVS 2019

Original document

The different versions of the original document can be found in:

• http://arxiv.org/abs/1907.09603

• http://arxiv.org/pdf/1907.09603

• http://xplorestaging.ieee.org/ielx7/8884213/8887758/08887768.pdf?arnumber=8887768,

http://dx.doi.org/10.1109/cavs.2019.8887768

• https://dblp.uni-trier.de/db/journals/corr/corr1907.html#abs-1907-09603,

https://arxiv.org/pdf/1907.09603.pdf,

https://arxiv.org/abs/1907.09603,

http://ui.adsabs.harvard.edu/abs/2019arXiv190709603E/abstract,

https://academic.microsoft.com/#/detail/2982710983