Formale Beschreibung einer IEC 61499- Laufzeitumgebung unter Berücksichtigung von Echtzeitanforderungen und dem unterlagerten Betriebssystem

Abstract

Der Einsatz von Verifikation wird in der heutigen Zeit in industriellen Unternehmen ein immer wichtiger werdender Punkt für die Erkennung und Eliminierung von Fehlern vor Beginn der Produktion von Produkten. Anhand von Verifikationsmethoden können diese Fehler vermieden werden, was zu einer Senkung der Entwurfskosten führt.<br />Mit dieser Arbeit wird eine formale Beschreibung einer IEC 61499 Laufzeitumgebung und einem darunter liegenden Betriebssystem durchgeführt, wobei die Eigenschaft der Echtzeitfähigkeit einfließt. Für die formale Verifikation wird die Methode des Model-Checking angewandt.<br />Mit dem Model-Checking werden formale Modelle auf dessen Verhalten und Spezifikation überprüft.<br />Nach einem theoretischen Einblick in die IEC 61499 µCrons Laufzeitumgebung des Instituts für Automatisierungs- und Regelungstechnik an der Technischen Universität Wien und in das Echtzeitbetriebssystem eCos wird ein Konzept für die Erstellung der jeweiligen formalen Modelle erarbeitet. Dabei wird der Modellierungsansatz der Net Condition Event Systems verwendet, da diese im Zusammenhang mit dem Standard IEC 61499 die größte Verbreitung haben.<br />Bei der Modellierung wurde auf einen sequentiellen Ereignisfluss geachtet, um mittels Verzögerungen die reale Abarbeitungszeit erfassen zu können.<br />Unter Verwendung von Aktivitätsdiagrammen werden anfangs die erstellten formalen Modelle präsentiert. Es wird auf dessen Konzepterstellung und Verhalten eingegangen. Neben der Realisierung und Beschreibung der formalen Modelle für die Laufzeitumgebung und das Betriebssystem, wird im besonderen auch auf deren Zusammenspiel eingegangen. Die Arbeit wird mit der Modellierung eines Anwendungsbeispiels abgeschlossen, wo ein Funktionsblocknetzwerk über zeitgesteuerte und extern getriggerte Ereignisse angesteuert wird. Unter Durchführung von unterschiedlichen Abfragen wird die Anwendung auf deren Korrektheit und Verhalten überprüft.<br />

The use of verification nowadays becomes more and more important in industrial enterprises. This is because it helps to identify and eliminate the errors before the start of the production. These errors can be avoided by means of the verification methods, which at the same time can lead to decreasing development costs.<br />This thesis realises a formal description of an IEC 61499 runtime environment and an underlying operation system, whereas the attribute of real-time capabilities is incorporated. The method of model-checking is used for the formal verification. The formal models are checked by use of this method for their behaviour and specification.<br />Primarily a theoretical overview of the IEC 61499 µCrons runtime environment established by the automation and control institute at Technical University of Vienna and the real-time operation system eCos is given. Afterwards a concept for the realisation of respective formal models is elaborated. For the realisation of the formal models a modelling approach of Net Condition Event Systems is used. The reason for this is that they are often used in connection with the standard IEC 61499. During the modelling it was important to pay attention to the sequential event flow, because of the registration of the real execution time by the means of delays.<br />The development of the formal models is presented using activity diagrams. The elaboration of concept and behaviour are shown more detailed. Behind the realisation and the description of the formal models for the runtime environment and the operation system, attention is turned especially to their interaction. The thesis is concluded with the modelling of an example for an application, where a function block network is driven through time triggered and externally triggered events. This application is checked for its correctness and behaviour using different enquiries.