A research team consisting of Tsutomu Kobayashi, Ichiro Hasuo, Fuyuki Ishikawa, and Shinya Katsumata at the National Institute of Informatics (NII, Japan) and Rick Salay and Krzysztof Czarnecki at University of Waterloo (Canada) developed a method that automatically transforms models of controller software into models that satisfy safety requirements even when there is uncertainty in sensing the state of the environment.
In addition to the transformation, the method generates formulas that represent the degree of uncertainty that the controller software can tolerate. The method can be applied to various controller systems that interact with the external environment, including autonomous vehicles.
This research was conducted under the ERATO MMSD Project (*1) funded by the Japan Science and Technology Agency (JST, Japan). The findings were presented at the 13th NASA Formal Methods Symposium (online) on May 26th, 2021. [Read more…] about Transformation of controller software to ensure safe behavior under perceptual uncertainty