Formale Analyse des Zeitverhaltens Netzbasierter Automatisierungssysteme

  • 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.
  • 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.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Jürgen Greifeneder
URN (permanent link):urn:nbn:de:hbz:386-kluedo-21542
ISBN:978-3-8322-6835-0
Advisor:Georg Frey
Document Type:Doctoral Thesis
Language of publication:German
Year of Completion:2007
Year of Publication:2007
Publishing Institute:Technische Universität Kaiserslautern
Granting Institute:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2007/11/02
Tag:DesLaNAS ; Netzbasierte Automatisierungssysteme ; PTA; Synchronisation zyklischer Prozesse ; wahrscheinlichkeitsbasierte Modellverifikation
DesLaNAS ; Networked Automation Systems ; probabilistic model checking ; probabilistic timed automata; synchronization of cyclic processes
GND-Keyword:Automatisierungssystem ; Model checking; Netzwerk ; Response-Zeit ; Stochastischer Automat
Faculties / Organisational entities:Fachbereich Elektrotechnik und Informationstechnik
DDC-Cassification:620 Ingenieurwissenschaften und zugeordnete Tätigkeiten

$Rev: 12793 $