Latest News


Mathematical Proof of Safety for Self-Driving Cars: A New Method Devised by NII Research Team


As part of the ERATO Mathematics for System Design Project (ERATO MMSD; a JST Strategic Basic Research Program), a research team led by Professor Ichiro Hasuo of the Information Systems Architecture Science Research Division, the National Institute of Informatics (NII), has developed a basic theory and technology to provide strong mathematical guarantees for the safety of automated driving systems for automobiles. The research results were published in the online version of IEEE Transactions on Intelligent Vehicles on July 5.

A proof-based approach to automated driving safety, shared by RSS and NII's proposed method, GA-RSS
Provided by NII

To promote the adoption of automated driving technologies in automobiles, it is not enough to simply improve automation safety. High levels of safety must also be guaranteed to society, and a level of understanding provided to the public to ensure acceptance of automated driving. However, the empirical and statistical approaches used up to now have been accompanied by questions such as "How can we say it is safe enough?" and "Can we provide convincing explanations to the public?" Therefore, experts in this field have hoped to create a logical approach to these issues, making the safety of automated driving easier to understand.

This is where RSS (responsibility-sensitive safety), a methodology proposed by Intel Corporation, has come into the spotlight. RSS aims to provide mathematical proof for the safety of automated vehicles by turning rules for traffic safety into precise mathematical formulas, then proving the validity of these formulas.

While it is generally difficult to mathematically prove the safety of complex systems such as automated driving, RSS makes this possible by focusing the evidence on logical safety rules that automated vehicles must follow. However, although industry and academia have shown significant interest in RSS, a technical basis for formulating and proving logical safety rules has yet to be developed. The application scope has also been limited to simple driving scenarios, such as following a car on a non-branching road.

To overcome this weakness, the NII research team has utilized its expertise in formal logic to establish a new technical foundation for RSS. It has used this foundation to propose GA-RSS, a new extension to RSS. Conventional RSS can only be used for collision avoidance in simple driving scenarios. By comparison, GA-RSS can formulate logical safety rules and prove they are correct even for complex driving scenarios that require achieving goals such as making an emergency stop at a safe location while avoiding a collision with another vehicle.

This approach proposes mathematically rigorous, logical safety rules, using a safety theorem to prove mathematically that accidents cannot occur as long as these rules are followed. As a technical basis for enabling this extension, the team proposed a new formal logic system named differential Floyd-Hoare logic (dFHL). It also designed and implemented a workflow and software for deriving logical safety rules based on this system.

Combining RSS with dFHL enables the GA-RSS extension, which can be applied to various automated driving situations. Taking emergency stops as an example, conventional RSS safety rules enforce short-sighted collision avoidance behavior. This limitation means that movements like lane changes cannot be executed to avoid interference with other vehicles, preventing the goal of an emergency stop. In contrast, GA-RSS safety rules can incorporate an overarching plan of action to pass other vehicles by accelerating or braking, thus achieving the goal of an emergency stop.

However, these logical safety rules need to be developed and proven individually for large numbers of driving scenarios. Using the rule derivation workflow and supporting software resulting from this project, it is realistic to develop logical safety rules for complex scenarios after a few weeks' work.

Logical safety rules created in this manner are generalized and independent of factors such as the manufacturer or car model, making them usable for many years as an asset for society.

As part of the ERATO MMSD project, the team will utilize the proposed workflow and support software to develop logical safety rules for more driving scenarios. In addition, it will continue theoretical research and software development to improve efficiency further and reduce the labor involved in developing logical safety rules.

This article has been translated by JST with permission from The Science News Ltd.( Unauthorized reproduction of the article and photographs is prohibited.

Back to Latest News

Latest News

Recent Updates

Most Viewed