GF_JG_DCDS_jun_2007

Greifeneder, J.; Frey, G.:
Probabilistic Timed Automata for Modeling Networked Automation Systems.
Preprints of the 1st IFAC Workshop on Dependable Control of Discrete Systems DCDS, pp. 143-148, Cachan, France, June 2007.

Abstract: 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.

Keywords: Networked Automation Systems, Formal Verification, Modeling, Automata