JG_Diss_2007

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

Dissertation, Technische Universität Kaiserslautern, Kaiserslautern, Germany, Nov. 2nd, 2007

Shaker-Verlag, Aachen, Dec. 2007, ISBN: 978-3-8322-6835-0

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.

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.

Schlagwörter: Wahrscheinlichkeitsbasierte Modellverifikation, stochastische zeitbewertete Automaten, Antwortzeiten, Beschreibungssprache DesLaNAS, Synchronisation zyklischer Prozesse, Netzbasierte Automatisierungssysteme

Download (Deutsche Nationalbibliothek, Frankfurt)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by the author or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by the author’s copyright. These works or parts of it may not be used to repost reprint/republish or for creating new collective works for resale or redistribution to servers or lists without the explicit permission of the copyright holder.