Summary
International Symposium on Nonlinear Theory and Its Applications
2022
Session Number:C2L-D
Session:
Number:C2L-D-01
Black Box Checking of Mobile Robot Path Planning Satisfying Safety Hyperproperties
Naomi Kuze , Keiichiro Seno , Toshimitsu Ushio,
pp.450-453
Publication Date:12/12/2022
Online ISSN:2188-5079
Summary:
A k-safety hyperproperty is a hyperproperty that is characterized by bad prefixes. For example, it can express security policies for safety-critical and safety-related systems. Black box checking (BBC) is a promising formal verification method of systems whose internal structure is unknown. However, a BBC method for verifying hyperproperties has not been considered yet. We extend a BBC for k-safety hyperproperties, and apply it to verification of a security policy for path planning of a mobile robot, and demonstrate it with an illustrative example.