Supervisory controller synthesis and implementation for safety PLCs

The development of supervisory controllers for cyber-physical systems is a laborious and error-prone process. Supervisor synthesis enables control designers to automatically synthesize a correct-by-construction supervisor from a model of the plant combined with a model of the control requirements. From the supervisor model, controller code can be generated which is suitable for the implementation on a programmable logic controller (PLC). Supervisors for industrial systems that operate in close proximity to humans have to adhere to strict safety standards. To achieve these standards, safety PLCs (SPLCs) are used. For SPLC implementation, the supervisor has to be split into a regular part and a safety part. In previous work, a method is proposed to automatically split a supervisor model for this purpose. The method assumes that the provided plant model is a collection of finite automata. In this paper, the extension to extended finite automata is described. Additionally, guidelines are provided for modeling the plant and the requirements to achieve a favorable splitting. A case study on a rotating bridge is elaborated which has been used to validate the method. The case study spans all development steps, including the implementation of the resulting supervisor to control the real bridge.

Supervisor synthesis and throughput optimization of partially-controllable manufacturing systems

One of the challenges in the design of supervisors with optimal throughput for manufacturing systems is the presence of behavior outside the control of the supervisor. Uncontrollable behavior is typically encountered in the presence of (user) inputs, external disturbances, and exceptional behavior. This paper introduces an approach for the modeling and synthesis of a throughput-optimal supervisor for manufacturing systems with partially-controllable behavior on two abstraction levels. Extended finite automata are used to model the high abstraction level in terms of system activities, where uncontrollability is modeled by the presence of uncontrollable activities. In the lower abstraction level, activities are modeled as directed acyclic graphs that define the constituent actions and dependencies between them. System feedback from the lower abstraction level, including timing, is captured using variables in the extended finite automata of the higher abstraction level. For throughput optimization, game-theoretic methods are employed on the state space of the synthesized supervisor to determine a guarantee to the lower-bound system performance. This result is also used in a new method to automatically compute a throughput-optimal controller that is robust to the uncontrollable behavior.