Deterministic pushdown automata as specifications for discrete event supervisory control in Isabelle
| dc.contributor.advisor | Nestmann, Uwe | |
| dc.contributor.advisor | Raisch, Jörg | |
| dc.contributor.author | Schneider, Sven | |
| dc.contributor.grantor | Technische Universität Berlin | en |
| dc.contributor.referee | Nestmann, Uwe | |
| dc.contributor.referee | Raisch, Jörg | |
| dc.contributor.referee | Giese, Holger | |
| dc.contributor.referee | Kammüller, Florian | |
| dc.date.accepted | 2019-02-26 | |
| dc.date.accessioned | 2019-12-20T14:12:58Z | |
| dc.date.available | 2019-12-20T14:12:58Z | |
| dc.date.issued | 2019 | |
| dc.description.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. | en |
| dc.description.abstract | 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. | de |
| dc.identifier.uri | https://depositonce.tu-berlin.de/handle/11303/10372 | |
| dc.identifier.uri | http://dx.doi.org/10.14279/depositonce-9332 | |
| dc.language.iso | en | en |
| dc.relation.issupplementedby | https://doi.org/10.5281/zenodo.1412369 | en |
| dc.relation.issupplementedby | https://doi.org/10.5281/zenodo.1346258 | en |
| dc.rights.uri | http://rightsstatements.org/vocab/InC/1.0/ | en |
| dc.subject.ddc | 006 Spezielle Computerverfahren | de |
| dc.subject.other | program synthesis | en |
| dc.subject.other | discrete event controller synthesis | en |
| dc.subject.other | supervisory control | en |
| dc.subject.other | theorem prover Isabelle | en |
| dc.subject.other | pushdown automata | en |
| dc.subject.other | Programmsynthese | de |
| dc.subject.other | Reglersynthese für ereignisdiskrete Systeme | de |
| dc.subject.other | Ãœberwachungsregelung | de |
| dc.subject.other | Theorembeweiser Isabelle | de |
| dc.subject.other | Kellerautomaten | de |
| dc.title | Deterministic pushdown automata as specifications for discrete event supervisory control in Isabelle | en |
| dc.title.translated | Deterministische Kellerautomaten als Spezifikationen für ereignisdiskrete Überwachungsregelung in Isabelle | de |
| dc.type | Doctoral Thesis | en |
| dc.type.version | acceptedVersion | en |
| tub.accessrights.dnb | free | en |
| tub.affiliation | Fak. 4 Elektrotechnik und Informatik | de |
| tub.affiliation.faculty | Fak. 4 Elektrotechnik und Informatik | de |
| tub.publisher.universityorinstitution | Technische Universität Berlin | en |