Model-based availability analysis for automated production systems: A case study

Availability is among the most important characteristics of manufacturing systems since it affects the productivity of the system. Yet, we argue that current approaches are inadequate for thoroughly analyzing availability of such systems. In this paper, we present a novel approach for analyzing availability of automated production systems. This approach extends the system's normative specification with deviation models to represent the occurrence and effects of faults in system components, and specific models to precisely capture failure definitions and availability requirements. Based thereon, we show how the system's conformance to availability requirements can be verified automatically using the probabilistic model-checker Prism. To facilitate applicability of the approach, we provide basic building blocks for common fault occurrences, effects, and availability metrics. Moreover, we illustrate its applicability and benefits by evaluating the effects of using different positioning sensors on the availability of the Pick-and-Place Unit, a lab-scale demonstrator considered suitable for evaluations of novel research approaches. We argue that our approach is able to verify quantitative availability requirements while reducing redundant models, and thereby, potential inconsistencies.