Performance Analysis of Production Lines Through Statistical Model Checking

Design and maintenance of reliable manufacturing systems calls for the development of formal models that allow for performance analysis. We consider the class of manufacturing systems such that the production of a workpiece consists of a sequence of manufacturing stages performed by fault-prone, repairable, workstations, equipped with finite-sized input buffers. We name this kind of systems production lines. Relying on an expressive property specification formalism, namely the hybrid automata specification language, we introduce a framework that allows for 1) the automatic generation of stochastic Petri nets models of arbitrary sized production lines and 2) the generation of a number of sophisticated performance indicators (in terms of hybrid automata) for analysing the dynamics of a production line. We validate our approach by presenting a number of experiments executed by means of the statistical model checker Cosmos.