Greifeneder, Jürgen:
Formale Analyse des Zeitverhaltens Netzbasierter Automatisierungssysteme

Dissertation, Technische Universität Kaiserslautern, Kaiserslautern, Deutschland, 02. November 2007

Kurzfassung: Die Architekturen vieler technischer Systeme sind derzeit im Umbruch. Der fortschreitende Einsatz von Netzwerken aus intelligenten rechnenden Knoten führt zu neuen Anforderungen an den Entwurf und die Analyse der resultierenden Systeme. Dabei spielt die Analyse des Zeitverhaltens mit seinen Bezügen zu Sicherheit und Performanz eine zentrale Rolle. Netzbasierte Automatisierungssysteme (NAS) unterscheiden sich hierbei von anderen verteilten Echtzeitsystemen durch ihr zyklisches Komponentenverhalten. Das aus der asynchronen Verknüpfung entstehende Gesamtverhalten ist mit klassischen Methoden kaum analysierbar. Zur Analyse von NAS wird deshalb der Einsatz der wahrscheinlichkeitsbasierten Modellverifikation (PMC) vorgeschlagen. PMC erlaubt detaillierte, quantitative Aussagen über das Systemverhalten. Für die dazu notwendige Modellierung des Systems auf Basis wahrscheinlichkeitsbasierter, zeitbewerteter Automaten wird die Beschreibungssprache DesLaNAS eingeführt. Exemplarisch werden der Einfluss verschiedener Komponenten und Verhaltensmodi auf die Antwortzeit eines NAS untersucht und die Ergebnisse mittels Labormessungen validiert.

Abstract: Currently the architectures of many technical systems are undergoing considerable changes. The increasing use of networks connecting intelligent processor nodes leads to new requirements on the design and the analysis of the resulting systems. In this process, the analysis of temporal behavior with regards to safety and performance plays a central role. Networked Automation Systems (NAS) differ from other distributed real-time systems due to the cyclic behavior of their components. The overall behavior arising from the asynchronous composition of these components is hardly analyzable with traditional methods. Therefore, the use of Probabilistic Model Checking (PMC) is proposed for the analysis of NAS. PMC allows detailed quantitative statements about the overall system behavior. For the modeling task, which is based on the use of probabilistic timed automata, the description language DesLaNAS is introduced. As a case study, the influence of different components and behavior modes on the response time of a typical NAS is analyzed. The results are validated by measured values.

Schlüsselworte:Wahrscheinlichkeitsbasierte Modellverifikation, stochastische zeitbewertete Automaten, Antwortzeiten, Beschreibungssprache DesLaNAS, Synchronisation zyklischer Prozesse, Netzbasierte Automatisierungssysteme

Download (Deutsche Nationalbibliothek, Frankfurt)