IJIE Article

Posted on August 1, 2015

A Model-Checking Based Approach to Robustness Analysis of Procedures under Human-Made Faults

Naoyuki Nagatou & Takuo Watanabe
International Journal of Industrial Engineering: Theory, Applications and Practice Vol. 22, No. 4, pp. 494-508, Aug., 2015.


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.


This article is an enhanced version of our conference paper presented at AP-BPM 2014.