Fault Tree Analysis(FTA) is a means for analyzing causes of hazards. The result of the analysis is a set of combinations of component failures that can result in a specific malfunction. FTA is useful to analyze safety of systems. However, it is a manual process and was not supported by systematic construction process, so fault tree can be inconsistent or insufficient. Unfortunately, there have not been appropriate methods to verify or assure correctness of fault trees.
Model-checking is one of the most successful techniques for automatic verification of concurrent finite-state systems and has been usually used to verify whether system design satisfies some properties. In this paper, we propose the way of correcting a fault tree using model checking.
To compensate a fault tree, we make formulas for nodes in fault tree and then, verify the formulas with real-time model checker UPPAAL. We analyze the result of verification and reflect the result to the fault tree.
폴트 트리 분석(Fault Tree Analysis)은 시스템의 위험 요소의 원인들을 분석해 나가는 도구이며, 이 분석의 결과는 특정한 이상기능에 대해 그것을 일으키는 원인이 되는 컴포넌트들의 조합이다. 폴트 트리 분석은 시스템의 안전성을 분석하는데 유용한 도구로 쓰여져 왔다. 그러나, 이 방법은 보통 수작업으로 이루어지며, 체계적인 구성 방법 없는 실정이어서 폴트 트리들은 부정확하게 또는 불충분하게 만들어질 수 있다. 불행히도 이제까지 폴트 트리의 정확성에 대해 검증하려는 시도들은 이루어지지 못했다.
모델 체킹은 유한 상태 시스템에 대한 매우 성공적인 자동 검증 방법 중 하나이다. 모델 체킹 방법은 보통 시스템 디자인이 특정한 속성들을 만족시키는가를 검증하는데 사용된다. 본 논문에서는 모델 체킹(Model Checking) 방법을 이용하여 폴트 트리를 좀 더 정확하게 보정하는 방법을 제안한다.
폴트 트리를 정확히 고치기 위해서, 먼저 폴트 트리의 노드에 대해서 공식을 만들고, 이 공식을 실시간 모델 체커 UPPAAL을 이용해 검증한다. 그리고 나서, 검증 결과를 분석하며, 이를 통해 얻어진 정보를 이용해 폴트 트리에 반영하게 된다.
