Die detaillierte quantitative Verifikation von netzwerkbasierten Automatisierungssystemen g
ewinnt durch die schnelle Ausbreitung von Ethernet-technologien eine stetig steigende Bedeutung, da die
entstehenden Systeme sowohl zeitkritische, deterministische als auch stochastische Anteile enthalten und
somit mit klassischen Methoden nicht mehr analysierbar sind. In diesem Beitrag wird ein Ansatz zur modularen
Modellierung netzwerkbasierter Automatisierungssysteme, deren Abbildung auf die für den verwendeten
probabilistischen Verifikationsansatz notwendigen formalen Beschreibungen (zeitbewertete Markovketten und PCTL),
sowie die Definition eines Qualitätsbegriffes vorgestellt.
Zur besseren Veranschaulichung wird die diskutierte Theorie anhand eines für die Automatisierungstechnik typischen
Anwendungsbeispiels demonstriert und die erhaltenen Ergebnisse anhand des Qualitätsmaßes diskutiert.
Quantitative Analysis of Response Times in Networked Automation Systems
The distribution of functionalities over a set of networked nodes results in a new type of automation
systems: Networked Automation Systems (NAS). These systems contain timed, deterministic as well as
stochastic parts and therefore are not analyzable using classical methods. In this paper a definition
of Quality of Control as well as an approach for the associated quantitative analysis of NAS using
probabilistic models and properties - Probabilistic Model Checking - is presented. To illustrate
the approach it is applied to several NAS-examples and discussed on means of quality.
Keywords: Probabilistic Model Checking, Quality, Networked Automation Systems, Quality of Control.