Reasoning about safety, security, and other dependability attributes of autonomous systems is a challenge that needs to be addressed before the adoption of such systems in day-to-day life. Formal methods is a class of methods that mathematically reason about a system's behavior. Thus, a correctness proof is sufficient to conclude the system's dependability. However, these methods are usually applied to abstract models of the system, which might not fully represent the actual system. Fault injection, on the other hand, is a testing method to evaluate the dependability of systems. However, the amount of testing required to evaluate the system is rather large and often a problem. This vision paper introduces formal fault injection, a fusion of these two techniques throughout the development lifecycle to enhance the dependability of autonomous systems. We advocate for a more cohesive approach by identifying five areas of mutual support between formal methods and fault injection. By forging stronger ties between the two fields, we pave the way for developing safe and dependable autonomous systems. This paper delves into the integration's potential and outlines future research avenues, addressing open challenges along the way.

翻译：推理自主系统的安全性、可靠性和其他可信属性，是此类系统在日常应用前亟待解决的挑战。形式化方法是一类通过数学推理分析系统行为的方法，因此正确性证明足以支撑系统可信性的结论。然而，此类方法通常应用于系统的抽象模型，可能无法完整表征实际系统。另一方面，故障注入是一种评估系统可信性的测试方法，但所需执行的测试量往往过大且成为难题。本愿景论文提出形式化故障注入方法——即将两种技术贯穿于开发全生命周期融合，以增强自主系统的可信性。我们识别出形式化方法与故障注入之间五个相互支撑的领域，倡导更具协同性的方案。通过强化两个领域的关联，为开发安全可靠的自主系统铺平道路。本文深入探讨了这种融合的潜力，并展望未来研究方向，同时阐明当前面临的开放性挑战。