Abstract: This paper investigates the application of probabilistic model checking to the analysis of Networked Automation Systems (NAS). Besides delay generating system structures due to shared component, asynchronously executed cyclic processes, and network transfers hard bounds on response time have to be considered. To determine the response time a modeling method for NAS is introduced and compared to other concepts known from literature. It is based on Probabilistic Timed Automata and Discrete Time Markov Chains. The paper also illustrates the basics of Probabilistic Model Checking - a method used to prove properties on the Markov models built.
Keywords: Networked Automation Systems, Reliability Modeling, Stochastic Automata,
Discrete Time Markov Chains, Probabilistic Model Checking.
|Jürgen Greifeneder, 26.09.2006||Impressum|