Greifeneder, Jürgen; Frey, Georg:

Wahrscheinlichkeitsbasierte Modellverifikation Netzbasierter Automatisierungssysteme,
at Automatisierungstechnik, Oldenbourg, Band 55, Heft 12, Seiten 624-633, Dezember 2007.

Abstract: In diesem Artikel werden die Möglichkeiten von Probabilistic Model Checking als formale Methode zur Analyse von Netzbasierten Automatisierungssystemen (NAS) diskutiert. Hierbei wird zunächst ein Überblick über vor-handene Analysemethoden gegeben und anschließend die Anforderungen an eine Modellform für NAS analysiert. Es wird gezeigt, dass sich die Verlässlichkeitsanalyse von NAS auf die Diskussion von Antwortzeiten zurückfüh-ren lässt. Anhand eines für die Automatisierungstechnik typischen Anwendungsbeispiels wird schrittweise der Einfluss unterschiedlicher Effekte auf die Performanz erläutert und diskutiert.

Schlagwörter: Wahrscheinlichkeitsbasierte Modellverifikation, Automaten, Synchronisationsprobleme, Netzbasierte Automatisierungssysteme, Antwortzeiten, Qualität, Ausfälle, Sicherheit.

Probabilistic Model Checking of Networked Automation Systems

Abstract: In this article, the possibilities of Probabilistic Model Checking as a formal method for the analysis of Networked Automation Systems (NAS) are analyzed. First an overview on existing methods is given. Thereafter, the re-quirements on a modeling formalism for representing NAS are discussed. Furthermore, it is shown, that depend-ability analysis of NAS can be abstracted towards the discussion of response times. Based on a typical example from the area of NAS, the influence of different effects on the performance of the total system will be explained and discussed.

Keywords: Probabilistic Model Checking, Automata, Synchronization, Networked Automation Systems, Response times, Quality, Failures, Safety.