Availability is among the most important characteristics of manufacturing systems since it directly affects throughput, and, therefore, productivity of the system. Yet, we argue that current availability analyses are insufficient 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 which represent fault occurrences and effects of certain components. Furthermore, based on this extended system specification, it formalizes availability metrics and associated failure modes. The system's conformance to availability requirements is then verified by translating the model for the probabilistic model-checker PRISM. To facilitate applicability of this approach, we provide basic building blocks for common fault occurrences, effects, and availability metrics. Moreover, we illustrate the applicability and benefits of our approach by evaluating the effects of using different positioning sensors on the availability of the Pickand-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 modeling overhead and ensuring consistency among models.     «

Availability is among the most important characteristics of manufacturing systems since it directly affects throughput, and, therefore, productivity of the system. Yet, we argue that current availability analyses are insufficient 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 which represent fault occurrenc...     »