Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications, which are analogous to behaviors and requirements in system design and give us the means to verify and synthesize system behaviors with formal guarantees. This monograph provides a survey of the current state of the art on applications of formal methods in the autonomous systems domain. We consider correct-by-construction synthesis under various formulations, including closed systems, reactive, and probabilistic settings. Beyond synthesizing systems in known environments, we address the concept of uncertainty and bound the behavior of systems that employ learning using formal methods. Further, we examine the synthesis of systems with monitoring, a mitigation technique for ensuring that once a system deviates from expected behavior, it knows a way of returning to normalcy. We also show how to overcome some limitations of formal methods themselves with learning. We conclude with future directions for formal methods in reinforcement learning, uncertainty, privacy, explainability of formal methods, and regulation and certification.

翻译：形式化方法是指基于严谨数学方法的系统开发技术，在保障安全关键系统正确性方面发挥了关键作用。形式化方法的核心构件是模型与规范，这对应于系统设计中的行为与需求，使我们能够以形式化保证的方式验证和综合系统行为。本专著系统综述了形式化方法在自主系统领域应用的最新研究进展。我们考虑不同框架下的正确性保证综合方法，包括封闭系统、反应式系统和概率设置。除了在已知环境中综合系统，我们还探讨了不确定性概念，并使用形式化方法约束采用学习技术的系统行为。进一步，我们研究了带监控机制的系统综合——这是一种缓解技术，确保系统一旦偏离预期行为，能够找到恢复正常状态的方法。同时，我们展示了如何通过学习克服形式化方法自身的某些局限性。最后，本文展望了形式化方法在强化学习、不确定性处理、隐私保护、形式化方法的可解释性以及监管认证等领域的未来发展方向。