Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-9332
For citation please use:
Main Title: Deterministic pushdown automata as specifications for discrete event supervisory control in Isabelle
Translated Title: Deterministische Kellerautomaten als Spezifikationen für ereignisdiskrete Überwachungsregelung in Isabelle
Author(s): Schneider, Sven
Advisor(s): Nestmann, Uwe
Raisch, Jörg
Referee(s): Nestmann, Uwe
Raisch, Jörg
Giese, Holger
Kammüller, Florian
Granting Institution: Technische Universität Berlin
Type: Doctoral Thesis
Is Supplemented By: https://doi.org/10.5281/zenodo.1412369
https://doi.org/10.5281/zenodo.1346258
Language Code: en
Abstract: The problem of supporting the construction of software that is known to satisfy a set of given requirements is one of the grand challenges in software engineering. Herein, we focus on the field of control theory for systems with discrete states and event-based communication. In this field, controllers coordinate components given by a plant to ensure that the amalgamation of controller and plant executes a desired behavior. We focus on the supervisory control problem, which, given a plant and a specification, requires the synthesis of a controller in the form of a piece of software. The least restrictive satisfactory controllers to be synthesized are determined in this problem by the specification and additional well-formedness conditions. Similar problems also occurred in the field of computer science and it is of general importance in application domains such as in parallel, distributed, and embedded systems. We focus on the fully automatic synthesis of controllers using algorithms. These algorithms construct controllers that are realizable in software and correct-by-construction for the two aforementioned inputs. The applicability of these algorithms is limited by insufficient expressiveness of the formalisms used for plants and specifications. However, expressiveness can not be increased arbitrarily while maintaining solvability of the problem in terms of a synthesis algorithm that solves all problem instances. Our main contribution is a controller synthesis algorithm that synthesizes a DPDA controller when provided with a DFA plant model and a DPDA specification. This algorithm supersedes earlier algorithms synthesizing a DFA controller when provided with a DFA plant model and a DFA specification because DPDA are strictly more expressive than DFA. The increased expressiveness of DPDA compared to DFA allows for the specification and enforcement of more complex patterns of behavior. Initial approaches to mitigate limitations of our algorithm, such as its nontermination for some specifications stating requirements that are unreasonable from a control-theoretic perspective, are presented in the form of alternative constructions and optimizations. We employed the interactive theorem prover Isabelle for the formal verification of this controller synthesis algorithm to obtain trustworthy proofs, which are free of faults and omissions. The resulting Isabelle framework for the formalization and verification of algorithms outstrips existing similar frameworks in covered formalisms, semantical properties, and provided results and is designed to be highly extendable in these aspects. It covers the formalisms of DPDA, CFGs, and Parsers as well as the notions relevant for our controller synthesis algorithm such as the unmarked and marked languages, nonblockingness, and controllability. An evaluation of our algorithm implemented as the Java prototype CoSy shows promising efficiency. This evaluation was based on three examples from manufacturing employing DPDA specifications. Using these examples, we also demonstrate the application of three use cases of our algorithm for controller synthesis, controller verification, and input validation.
Das Problem, die Konstruktion von Software zu unterstützen, von der bekannt ist, dass sie bestimmte Anforderungen erfüllt, ist eine der großen Herausforderungen in der Softwareentwicklung. In dieser Arbeit konzentrieren wir uns auf das Gebiet der Regelungstheorie für Systeme mit diskreten Zuständen und ereignisbasierter Kommunikation. In diesem Gebiet koordinieren Regler die durch eine Strecke vorgegebenen Komponenten, um sicherzustellen, dass die Verschmelzung von Regler und Strecke ein gewünschtes Verhalten ausführt. Wir konzentrieren uns auf das Problem der Überwachungsregelung, das für eine Strecke und eine Spezifikation die Synthese eines Reglers in Form einer Software erfordert. Die am wenigsten restriktiven zufriedenstellenden Regler, die synthetisiert werden sollen, werden in diesem Problem durch die Spezifikation und zusätzliche Wohlgeformtheitsbedingungen bestimmt. Ähnliche Problemstellungen sind bedeutend auf dem Gebiet der Informatik in Anwendungsdomänen wie z.B. in parallelen, verteilten und eingebetteten Systemen. In der Arbeit konzentrieren wir uns auf die vollautomatische Synthese von Reglern mit Algorithmen. Diese Algorithmen konstruieren Regler, die in Software realisierbar sind und für die beiden oben genannten Eingaben die am wenigsten restriktiven zufriedenstellenden Regler erzeugen. Die Anwendbarkeit dieser Algorithmen ist durch eine unzureichende Ausdrucksmächtigkeit der für Strecken und Spezifikationen verwendeten Formalismen begrenzt. Die Ausdrucksmächtigkeit kann jedoch nicht beliebig erhöht werden, wenn die Lösbarkeit des Problems mittels eines Synthesealgorithmus, der alle Problemfälle löst, aufrechterhalten werden soll. Unser Hauptbeitrag ist ein Reglersynthesealgorithmus, der einen DPDA Regler synthetisiert, wenn ihm ein DFA Streckenmodell und eine DPDA Spezifikation übergeben werden. Dieser Algorithmus ersetzt frühere Algorithmen, die einen DFA Regler für ein DFA Streckennmodell und eine DFA Spezifikation synthetisieren, weil DPDA ausdrucksmächtiger als DFA sind. Die erhöhte Ausdrucksmächtigkeit von DPDA im Vergleich zu DFA ermöglicht die Spezifikation und Umsetzung komplexerer Verhaltensmuster. Erste Ansätze, um die Limitierungen unseres Algorithmus zu mindern, wie z.B. die Nichtterminierung für einige Spezifikationen, die aus einer kontrolltheoretischen Perspektive unangemessene Anforderungen enthalten, werden in Form von alternativen Konstruktionen und Optimierungen präsentiert. Wir verwendeten den interaktiven Theorembeweiser Isabelle zur formalen Verifikation dieses Reglersynthesealgorithmus, um vertrauenswürdige Beweise zu erhalten, die frei von Fehlern und Auslassungen sind. Das resultierende Isabelle Rahmenwerk für die Formalisierung und Verifikation von Algorithmen übertrifft bestehende ähnliche Rahmenwerke in Hinsicht auf abgedeckte Formalismen, semantischen Eigenschaften und erbrachte Ergebnisse. Es weißt in diesen Aspekten ein starkes Erweiterungspotential auf. Es behandelt die Formalismen von DPDA, CFGs und Parsern sowie die für unseren Reglersynthesealgorithmus relevanten Begriffe wie nicht markierte und markierte Sprachen, Nichtblockierung und Regelbarkeit. Eine Evaluierung unseres als Java Prototyp CoSy implementierten Algorithmus zeigt eine vielversprechende Effizienz. Diese Bewertung basiert auf drei Beispielen aus der Bereich der Fertigung unter Verwendung von DPDA Spezifikationen. Anhand dieser Beispiele demonstrieren wir auch die Nutzung von drei Anwendungsfällen unseres Algorithmus für die Reglersynthese, Reglerverifizierung und Eingabevalidierung.
URI: https://depositonce.tu-berlin.de/handle/11303/10372
http://dx.doi.org/10.14279/depositonce-9332
Exam Date: 26-Feb-2019
Issue Date: 2019
Date Available: 20-Dec-2019
DDC Class: 006 Spezielle Computerverfahren
Subject(s): program synthesis
discrete event controller synthesis
supervisory control
theorem prover Isabelle
pushdown automata
Programmsynthese
Reglersynthese für ereignisdiskrete Systeme
Überwachungsregelung
Theorembeweiser Isabelle
Kellerautomaten
License: http://rightsstatements.org/vocab/InC/1.0/
Appears in Collections:Fak. 4 Elektrotechnik und Informatik » Publications

Files in This Item:
schneider_sven.pdf
Format: Adobe PDF | Size: 3.6 MB
DownloadShow Preview

Item Export Bar

Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.