||A Model-Checking Based Approach to Robustness Analysis of Procedures under Human-Made Faults
A Model-Checking Based Approach to Robustness Analysis of Procedures under Human-Made Faults
永藤, 直行 ,
NAGATOU, NAOYUKI ,
渡部, 卓雄Watanabe, Takuo
International Journal of Industrial Engineering: Theory, Applications and Practice
508 , 2015-08
We propose a model-checking approach for analyzing the robustness of procedures that suffer from human-made faults. Many procedures executed by humans incorporate fault detection and recovery tasks to recover from human-made faults. Examining whether such recovery tasks work as expected is crucial for preserving the trust and reliability inherent in safety-critical domains. To achieve this, we used a type of fault-injection method that injects a set of human-made faults into a fault-free model of a given procedure; the fault set is selected according to Swain's discrete action classification. We use a model checker to determine paths to error states within the model and its properties formalized via CCS and LTL. We show the effectiveness of our method by investigating the recoverability of a real-world procedure.