Towards Formal Fault Injection for Safety Assessment of Automated Systems

要約

自律システムの安全性、セキュリティ、その他の信頼性属性について推論することは、そのようなシステムを日常生活に導入する前に対処する必要がある課題です。
形式的メソッドは、システムの動作を数学的に推論するメソッドのクラスです。
したがって、正確性の証明は、システムの信頼性を結論付けるのに十分です。
ただし、これらの方法は通常、システムの抽象モデルに適用されるため、実際のシステムを完全には表現していない可能性があります。
一方、フォールトインジェクションは、システムの信頼性を評価するテスト手法です。
ただし、システムを評価するために必要なテストの量はかなり多く、問題になることがよくあります。
このビジョン ペーパーでは、自律システムの信頼性を強化するために、開発ライフサイクル全体を通じてこれら 2 つの手法を融合した正式なフォールト インジェクションを紹介します。
私たちは、形式的手法とフォールト挿入の間の相互サポートの 5 つの領域を特定することにより、より一貫性のあるアプローチを提唱します。
2 つの分野間の連携を強化することで、安全で信頼できる自律システムの開発への道を切り開きます。
このホワイトペーパーでは、統合の可能性を掘り下げ、将来の研究の道筋を概説し、その過程で未解決の課題に対処します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google