Model Checking of Systems with Unreliable Machines Using PRISM
Xinze Huang, Zhenyuan Ding, Zijian Bi, Yili Wang, Kai Zheng, Xin Huang · 2018
A system with two machines and one buffer is common in many fields. However, the machines cannot be always stable. This paper introduces a system consisting of two unreliable machines and one buffer, which is applied in a manufacturing factory. The evaluation of its reliability and performance will be discussed using a model checking software called PRISM. The model is based on the Continuous-time Markov chain.