Modeling of Networked Automation Systems for simulation and model checking of time behavior

In terms of fulfilling the customers´ needs, Networked Automation Systems (NAS) have gained increasing significance in various industries, e.g. machine and plant automation over the past years. The advantages of NAS lie in enhanced dependability, flexibility and configurability, thereby overcoming various shortcomings of centralized automation systems. Besides, verification of the time behavior of NAS is still a challenge for engineers. There is a lack in an appropriate modeling notation for automation engineers as well in tool support to estimate or even verify the time behavior. This paper presents a method for modeling real-time requirements and properties of NAS and a concept for its combination with NAS simulation and mechanized verification. This enables the comparison of different architectures regarding their time behavior.