PROBABILISTIC TIMED AUTOMATA FOR MODELING NETWORKED AUTOMATION SYSTEMS

For the formal analysis of dependability of Networked Automation Systems (NAS) it is necessary to model the whole system first. Due to the probabilistic and distributed nature of the problem, a modular automata based approach is preferable for modeling and analysis. In this paper a formal automata definition for the specific needs of modeling NAS is given including continuous density distributions. For this model a discretization procedure as well as a transformation of the resulting discrete model into the input language of the probabilistic model checking software PRISM is presented. Finally an example is given, to illustrate the approach. The results of the automata based analysis are compared to measurements.