Formale Analyse des Zeitverhaltens Netzbasierter Automatisierungssysteme

Untersucht wird die Entwicklung von Methoden zum Entwurf und zur Analyse verteilter Automatisierungssysteme (Distributed Control System, DCS). Bei diesen Systemen wird neben den in klassischen Automatisierungssystemen vorhanden Faktoren Control und Computation auch die Communication wichtig (C³ Technologies). Die Untersuchung eines DCS hängt stark von der Art der Automatisierungsaufgabe ab und unterscheidet zwischen kontinuierlichen und den betrachteten diskreten Systemen (Discrete Event Systems, DES).

Formal Responsetime Analysis in Networked Automation Systems

The development of design and analysis methods for distributed control systems is examined in this work. Within these systems Communication in additon to control and Computation - which are already known from classical automation systems - becomes a third factor (C³ Technologies). The investigation of a DCS depends strongly on the kind of task of automation and discriminates between continuous and the discrete event systems discussed here.

Während die Automatisierung des Netzwerkverkehrs nach wie vor stark von der Informatik selbst geprägt ist, wird die Frage nach Netzwerktechniken für die Automatisierung i.d.R. von den Ingenieurwissenschaften getragen. Für ein gegebenes ereignisdiskretes verteiltes Automatisierungssystem (DDECS) sind unterschiedlichste Anforderungen zuzusichern. Neben die korrekte Funktionsweise tritt dabei vor allem die rechtzeitige Ausführung der verwendeten Algorithmen.

While the automation of network traffic is still strongly dominated by computer science, network techniques for automation are discussed by engineers. For a given distributed discrete event automation system (DDECS) different requirements have to be assured. Apart from the correct functioning mode, the timely execution of the used algorithms becomes an important factor.

Die in herkömmlichen Anlagen drahtbasierten Verbindungen zwischen den Controllern, Aktuatoren und Sensoren werden in zunehmedem Maße durch Übertragungskanäle mit paketvermittelnden Protokollen (LAN, WLAN, Bluetooth u.ä.) ersetzt. Die meisten Control-Aufgaben erfordern allerdings, dass die Control-Instanz mit den angeschlossenden Hardwarekomponenten (Aktuatoren und Sensoren) innerhalb fester Zeitschranken kommuniziert, da andernfalls die Control-Aufgabe nicht erreicht werden kann. Während dies für festverdrahtete Systeme lediglich Einfluss auf Zykluszeiten (und somit Prozessorgeschwindigkeiten) hat, müssen in verteilten Systemen die Signallaufzeiten ebenso Berücksichtigung finden, wie Netzausfälle und Überlastsituationen. Da sich beliebige Präzision technisch (finanzierbar) ebenso wenig realisieren lässt, wie absolute Ausfallsicherheit, werden aus den bekannten ja-nein-Aussagen wahrscheinlichkeitsbehaftete Feststellungen. So kann von einem System z.B. gefordert werden, dass ein bestimmter Signalwert in 95% der Fälle binnen einer bestimmten Zeit eine Reaktion an einem Ausgang hervorrufen muss.

In conventional control systems, all the connections between controllers, actuators and sensors are hard wired. In DDECS these connections are replaced by packet based communication channels like TCP/IP (LAN, WLAN) or Bluetooth. Most control instances require information from their hardware components (actuators and sensors) within hard bounded time intervals, since otherwise the control task cannot be achieved. While in hard-wired systems this has influence on cycle times (and thus processor speeds) only, signal delay times must be considered in DDECS as well as network downtimes and overload situations.

To avoid worst case analysis that often leads to infeasible demands on the control systems hardware the classical Yes-No-statements could be relaxed by introducing probabilistic bounds. This leads to properties like: With a probability of at least 99,9% a reaction to a change in a sensor value will be issued within 200ms.

Parallel zu den theoretischen Überlegungen konzentrierten sich die Forschungsarbeiten schwerpunktmäßig auf die Implementierungen dieser Modelle in der Software PRISM, einem propabilistic model checker der University of Birmingham. Mittels eines solchen model checkers kann die Wahrscheinlichkeit bestimmt werden, dass ein physikalisches System einen bestimmten Zustand einnimmt. Um aussagekräftige (i.S.v. differenzierte) Ergebnisse zu erhalten, muss es sich hierbei jedoch um nur singulär auftretende Zustände handeln, da sich bei zyklischem Auftreten die gesuchte Wahrscheinlichkeit als geometrische Reihe beschreiben lässt und somit gegen eins konvergiert. Im Rückschluss bedeutet dies, dass sich das zu untersuchende Modell erst aus der Überlagerung des physikalischen Modells mit der gesuchten Eigenschaft gewinnen lässt.

To answer questions like this, simulation is infeasible for complex systems since a probabilistic solution will need a very long simulation time. The problem is even bigger if the analysis is extended from a simple performance check to a detailed reliability analysis where the possibilities of failures in the components are considered during the analysis. In this case the system under consideration contains very short cycle times of a controller together with very long mean times between failures (MTBFs) of the components.

Parallel to the theoretical considerations the research work concentrates in the implementation of these models in the software PRISM, a probabilistic model checker from the University of Birmingham. Using such model checkers the probability that a physical system takes a certain condition can be determined. In order to receive meaningful results, only monotheistic states are useful, since the probabilistic of any state with cyclic occurrence can be described as geometrical row and thus converges against one. This means that the model examined can be determined only by superposing the physical model with the characteristic discussed.