论文标题
为自动海洋车辆的控制算法进行演绎验证
Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles
论文作者
论文摘要
在现实世界中，使用自动驾驶汽车的使用通常无法为其复杂控制器提供安全保证的困难。这些控制器的基于模拟的测试无法提供足够的安全保证，并且由于自动驾驶汽车的混合性质，正式验证的使用非常具有挑战性。我们进行的工作论文引入了一种正式的验证方法，该方法通过通过证明助手（Isabelle）将这种系统（以GNU/OCTAVE）的数值计算（以GNU/OCTAVE为单位）整合到其混合系统验证来解决这一挑战。为了显示我们方法的有效性，我们使用它来验证自动船舶汽车的差异不变性，并在多种模式之间进行控制器切换。
The use of autonomous vehicles in real-world applications is often precluded by the difficulty of providing safety guarantees for their complex controllers. The simulation-based testing of these controllers cannot deliver sufficient safety guarantees, and the use of formal verification is very challenging due to the hybrid nature of the autonomous vehicles. Our work-in-progress paper introduces a formal verification approach that addresses this challenge by integrating the numerical computation of such a system (in GNU/Octave) with its hybrid system verification by means of a proof assistant (Isabelle). To show the effectiveness of our approach, we use it to verify differential invariants of an Autonomous Marine Vehicle with a controller switching between multiple modes.
