학술논문
Formal analysis of production line systems by probabilistic model checking tools
Document Type
Conference
Author
Source
2021 26th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA ) Emerging Technologies and Factory Automation (ETFA ), 2021 26th IEEE International Conference on. :01-08 Sep, 2021
Subject
Language
Abstract
Performance modelling is a fundamental part of the design and operation of reliable manufacturing systems. Based on the probabilistic model checking formalism [11] supported by the PRISM tool [13], in this paper we present a framework for automatic generation of 1) formally expressed discrete-state Markov chain (DTMC) models of production lines, and 2) of a number of related key performance indicators given in terms of temporal logic formulae. Since the framework is fully parametric it can straightforwardly be used for comparative analysis of different system configurations. In order to tackle scalability issues we present two alternative encodings of the DTMC model corresponding to a given production system and discuss how they compare. We demonstrate the effectiveness of the framework through a number of experiments.