Deterministic pushdown automata as specifications for discrete event supervisory control in Isabelle
Sven Schneider · DepositOnce · 2019
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.