English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Technology advances give us the hope of driving without human error, reducingvehicle emissions and simplifying an everyday task with the future ofself-driving cars. Making sure these vehicles are safe is very important to thecontinuation of this field. In this paper, we formalize theResponsibility-Sensitive Safety model (RSS) for self-driving cars and prove thesafety and optimality of this model in the longitudinal direction. We utilizethe hybrid systems theorem prover KeYmaera X to formalize RSS as a hybridsystem with its nondeterministic control choices and continuous motion model,and prove absence of collisions. We then illustrate the practicality of RSSthrough refinement proofs that turn the verified nondeterministic controlenvelopes into deterministic ones and further verified compilation to Python.The refinement and compilation are safety-preserving; as a result, safetyproofs of the formal model transfer to the compiled code, while counterexamplesdiscovered in testing the code of an unverified model transfer back. Theresulting Python code allows to test the behavior of cars following the motionmodel of RSS in simulation, to measure agreement between the model andsimulation with monitors that are derived from the formal model, and to reportcounterexamples from simulation back to the formal model.

Slow Down, Move Over: A Case Study in Formal Verification, Refinement,  and Testing of the Responsibility-Sensitive Safety Model for Self-Driving  Cars