论文标题
网络物理系统中端到端学习的正式验证：进步和挑战
Formal Verification of End-to-End Learning in Cyber-Physical Systems: Progress and Challenges
论文作者
论文摘要
自主系统（例如自动驾驶汽车，自动驾驶无人机和自动火车）必须具有强大的安全保证。在过去的十年中，基于正式方法的技术在为包括操作系统内核，加密协议和无人机控制软件在内的大型软件系统提供强大的正确性保证方面取得了成功。这些成功表明，可以通过构建正式的，由计算机检查的正确性证明来确保自主系统的安全。本文确定了现有正式验证技术的三个假设，解释了这些假设中的每一个如何限制验证在自主系统中的适用性，并总结了在提高正式验证提供的证据强度方面的初步工作。
Autonomous systems -- such as self-driving cars, autonomous drones, and automated trains -- must come with strong safety guarantees. Over the past decade, techniques based on formal methods have enjoyed some success in providing strong correctness guarantees for large software systems including operating system kernels, cryptographic protocols, and control software for drones. These successes suggest it might be possible to ensure the safety of autonomous systems by constructing formal, computer-checked correctness proofs. This paper identifies three assumptions underlying existing formal verification techniques, explains how each of these assumptions limits the applicability of verification in autonomous systems, and summarizes preliminary work toward improving the strength of evidence provided by formal verification.
