Probabilistic Model Checking for IEC 61499: A Manufacturing Application

The ever-increasing complexity of industrial control systems generates a demand for reliable development methods. IEC 61499, a recent industrial standard, helps to develop complex distributed systems based on their positive characteristics, namely reusability, reconfigurability, interoperability, and portability. Formal verification techniques, such as model checking, have been proposed to ensure the correctness of these systems during the design time. However, they do not consider the presence of the environment that can impact the application behaviour at runtime. This work combines design time and runtime analyses to apply probabilistic model checking on an IEC-61499-based manufacturing application. We present several probabilistic properties to be checked. The results are visualised graphically to be analysed, which allows one to optimise the system's quantitative features, such as productivity.