Komponentenbasierte Überwachung hybrider Systeme durch den Einsatz formaler Methoden

Mekacher, Leila

Vorschau

PDF
Dissertation.pdf - Veröffentlichte Version
Download (56MB)

URL:	https://madoc.bib.uni-mannheim.de/41516
URN:	urn:nbn:de:bsz:180-madoc-415167
Dokumenttyp:	Dissertation
Erscheinungsjahr:	2016
Ort der Veröffentlichung:	Mannheim
Hochschule:	Universität Mannheimm
Gutachter:	Atkinson, Colin
Datum der mündl. Prüfung:	17 November 2016
Sprache der Veröffentlichung:	Deutsch
Einrichtung:	Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik > Software Engineering (Atkinson 2003-)
Fachgebiet:	500 Naturwissenschaften
Normierte Schlagwörter (SWD):	Überwachung , Schätztheorie , Hybrides System , Petrinetz , Formale Sprache , Komponentenmodell
Freie Schlagwörter (Englisch):	Formal methods , petri nets , component-based systems , monitoring , probabilistic framework , dependability
Abstract:	Die vorliegende Arbeit beschäftigt sich mit der Entwicklung eines neuen Verfahrens zum nahtlosen Komponentenentwurf und zur Systemüberwachung durch ein einheitliches Modell, das die Anforderungen der Entwicklung von komplexen dynamischen Systemen erfüllt und somit einen Beitrag zum Entwurf verlässlicher Systeme leistet. Hierfür wird die komponentenbasierte Design-Methodologie KobrA eingesetzt, weil diese eine schrittweise Komponentenzerlegung auf verschiedenen Abstraktionsebenen und Sichten durchführt. Sie beinhaltet sowohl „Top-down“-Elemente als auch „Bottom-up“-Ansätze, die für eine effiziente prototypische Systemrealisierung geeignet sind. Mit der Entwicklung eines formalen echtzeitfähigen Überwachungs- und Fehlererkennungsmechanismus wird die KobrA-Methode durch eine formale Modellierungssprache erweitert, welche sowohl für die Softwareentwickler als auch für die Ingenieure verständlich sein soll. Aus diesem Grund sollte diese Sprache eine eindeutige und streng definierte Semantik besitzen. Die einheitliche Beschreibung der Systemkomponenten sowie der Überwachungskomponenten durch denselben formalen Sprachmittel ermöglicht die systematische Einbettung der Überwachung über den gesamten Entwicklungsprozess und dessen Ausführung während des Betriebs. Petri-Netze gehören zur Graphentheorie und zählen seit mehreren Jahren zu den mächtigsten Spezifikationswerkzeugen in verschiedenen Gebieten. Sie erlauben die Beschreibung des Komponentenverhaltens durch ein Netzwerk, bestehend aus Knoten und aus Bedingungen für den Datenfluss zwischen diesen Knoten. Wesentliche Vorteile von Petri-Netzen sind zum einen ihre formale mathematische Formulierung, die auf einem soliden theoretischen Fundament beruht, sowie zum anderen die explizite Abbildung des Prozesszustandes über ein Markierungskonzept. Petri-Netze ermöglichen zusätzlich die Darstellung sequentieller, sich gegenseitig ausschließender sowie paralleler Aktivitäten, die Modellierung und Visualisierung von Systemverhalten sowie die Nebenläufigkeit und die Synchronisation von kooperativen Prozessen. In dieser Arbeit erfolgt die Verhaltensbeschreibung der Überwachungskomponenten durch eine neue Klasse von Petri-Netzen, so genannte „Modifizierte Partikel Petri-Netze“ (engl., Modified Particle Petri Nets „MPPN“). Diese Netzklasse beinhaltet hybride Petri-Netze für die Modellierung des hybriden Systemverhaltens und einen Partikelfilter als probabilistische Erweiterung, um die Überwachung als Tracking-Problem aufzufassen. Petri-Netze bieten eine vollständige und konsistente Beschreibung der Prozesse, die graphische Anschauung sowie Simulation und Animation als Testmöglichkeit bereits während der Entwurfsphase. Die Kombination aus KobrA-Beschreibungsformalismus und Petri-Netzen erlaubt eine anschauliche, modular und hierarchisch strukturierte Modellierung, direkt in einer formalen Sprache. Durch unterstützende Werkzeuge, die im Rahmen dieser Arbeit entwickelt sind, kann die Realisierung der Überwachungskomponente direkt aus der Spezifikation generiert werden. Hierfür wird das Petri-Netzmodell in ein textuelles kompaktes XML-Austauschformat (engl., „Extensible Markup Language“) transformiert, welche sich an dem PNML-Standard (engl., „Petri Net Markup Language“) orientiert. Diese generische Vorlage enthält das Komponentenverhalten und die für den Überwachungsprozess notwendigen Parameter. Der besondere Aspekt für den Einsatz derselben formalen Methode, nämlich die Petri-Netze, sowohl für die Spezifikation als auch für die Realisierung, beruht auf zwei Zielen. Das primäre Ziel ist, ein einheitliches verständliches Ausdrucksmittel für die Entwurfsphase eines Systems zu stellen, mit dem alle Aspekte des ausgewählten Abstraktionsniveaus unmissverständlich dargestellt werden können. Denn Spezifikationsdokumente in natürlichen Sprachen sind anfällig für Missverständnisse, während formale Spezifikationen auf mathematischen Beschreibungen und eindeutiger Semantik und Syntaxen basieren. Das sekundäre Ziel ist eine formale überprüfbare Spezifikation (mittels eines Simulationswerkzeuges) als solide Basis für die Realisierungsphase zu bilden. Denn eine automatisch verifikationsbasierte Systementwicklung stellt eine Möglichkeit zur Erhöhung der Systemverlässlichkeit dar. Die andere Möglichkeit basiert auf der Robustheit des Überwachungsverfahrens während der Betriebsphase.
Übersetzung des Abstracts:	This thesis deals with the development of a new method for seamless component design and system monitoring based on a unified dependability model suitable for developing complex dynamic systems. It therefore advances the state-of-the-art in designing dependable systems. The underlying methods used for this purpose is the component-based design methodology KobrA since it support the systematic analysis and decomposition of components at different levels of abstraction and granularity. It also supports both “top-down” as well as “bottom-up” approaches that are suitable for developing efficient prototype system realizations. To provide a formal real-time monitoring and fault detection mechanism, in this thesis the KobrA-method is enhanced with a formal modeling language designed to be understandable to both software developers and system engineers. The desired language should not only have a unique and strictly defined semantics it should support a unified description of the system components and monitoring components that allows the systematic integration of the monitoring over the entire development process as well as its execution during operation. The underling formalism is based on Petri nets – powerful graph theoretical models that have been used in many different areas of software development for many years. They allow the description of component behavior and the conditions for the data flow through a network of nodes. The main advantages of Petri nets are firstly their formal mathematical formulation based on a solid theoretical foundation, and secondly, their ability to explicitly illustrate processes via a labeling concept. Petri nets also allow the representation of sequential and concurrent activities, the modeling and visualization of system behavior, and the synchronization of cooperative processes. In this thesis the behavioral description of the monitoring components is achieved through a new class of Petri nets called “Modified Particle Petri Nets – MPPN”. This new class includes hybrid Petri nets for modeling the hybrid system behavior and a probabilistic “particle filter” extension to allow the monitoring process to be treated as a tracking problem. Petri nets not only support the complete and consistent description, graphical representation and simulation of processes it also support animation-based testing as early as the design phase. The combination of KobrA’s description formalism and Petri nets supports the intuitive, modular and hierarchical modeling of component-based systems in a formal way. Supporting tools developed as part of this work allow the realization of the monitoring component to be generated directly from the specification. For this purpose, the Petri net model is transformed into a compact, textual XML interchange format (eng., "Extensible Markup Language"), which is based on the PNML standard (eng., "Petri Net Markup Language"). This generic template includes the components’ behaviors and the necessary parameters for the monitoring process. There are two main motivations for the use of a single formal method, Petri nets, for both the specification and the implementation of component-based systems. The primary objective is for the system design to be described using a unified, clear language supporting the representation of all aspects at different levels of abstraction without any ambiguities or potential for misunderstandings. While specification documents in natural languages are prone to misinterpretations, this is not the case with formal specifications which are based on mathematical foundations and unambiguous semantics and syntaxes. The secondary objective is to obtain formally verified (by means of a simulation tool) specifications to provide a solid basis for the implementation phase. The automatically verified designs that result not only increase the inherent dependability of systems by reducing implementation errors they also provide the basis for robust, real-time monitoring of system execution during the operating phase. (Englisch)