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, 2015, 22(4): 494-508.

• human-made fault
• model checking
• dependability
• robustness
• linear temporal logic
• process algebra

A model-checking approach to analyze the robustness of procedures that suffer from human-made faults is proposed. 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 to preserve the trust and reliability inherent in safety-critical domains. To achieve this, we have employed a fault-injection method that injects a set of human-made faults into a fault-free model for a given procedure. This fault set is selected according to Swain's discrete action classification. The proposed approach uses a model checker to determine paths to error states within the model, and its properties are formalized via calculus of communicating systems and linear temporal logic. The effectiveness of the proposed method is demonstrated by investigating the recoverability of a real-world procedure.

• 出版日期2015