Control Synthesis for Batch Processes

Batch applications form an important application class within the field of process industries. In this thesis we propose multiple models, frameworks and design concepts in order to apply formal methods to the control synthesis in batch control. The thes is can be divided into two main parts. The first part develops a framework for the modeling of hybrid (mixed continuous/discrete) systems. A control engineering view of the system is taken, distinguishing between an uncontrolled hybrid plant and a hybrid plant and a hybrid controller unit that controls the plant in a closed-loop fashion. Combining the modeling power of the hybrid system with the principles of object-orientation, the concept of hybrid objects is introduced. Hybrid objects are general, reusable and encapsulated models of physical systems. The notion of controllability for hybrid systems is introduced and a semi-decidable algorithm for the restricted class of integrator hybrid systems is presented. The algorithm automatically generates correct control code given the desired behavior of the object. Furthermore, hybrid objects are shown to be well suited to model the hybrid behavior of batch processes on a more detailed level, allowing also hybrid, behavioral specifications on the process behavior. The second part looks at batch processes from the modeling and resource allocation point of view and is aimed at the construction of a discrete supervisor that is able to coordinate and control several recipes within the same plant. After proposing a complete framework of general resource models, the control synthesis process is divided into two parts: static and dynamic resource allocation, including booking strategies and synchronization issues between resources. Both design activities require information about deifferent aspects of the system and, hence, different models. We note that the here presented formulation of the synchronization issues between resources is new. Starting with the topology of the plant and the functional potential of its different resources on one hand, and a general, device-independent recipe on the other, the functional requirements of the recipe are algorithmically mapped onto the different r esources of the plant. The result is a device-dependent recipe, which represents all possible ways the plant can be utilized in order to produce the desired batch. As a next step, this recipe is augmented with booking strategies and translated into a non-deterministic Petri net. Using an extension of the supervisory control theory, a discrete supervisor for the plant, which guarantees correct and parallel execution of the recipes, is generated