AP-BPM2014 Talk

Posted on July 3, 2014

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

Naoyuki Nagatou &Takuo Watanabe
2nd Asia Pacific Conference on Business Process Management (AP-BPM 2014),
Queens University of Technology, Brisbane, Australia, 2014/7/3-4.

Abstract

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

Publication

Naoyuki Nagatou & Takuo Watanabe, A Model-Checking Based Approach to Robustness Analysis of Procedures under Human-Made Faults, In Asia Pacific Business Process Management, Lecture Notes in Business Information Processing, Vol. 181, pp. 117-131, Springer, DOI: 10.1007/978-3-319-08222-6_9, Jul., 2014.

An enhanced version of this paper is published as a journal article.