Guided Synthesis of Control Programs Using UPPAAL

In this paper we address the problem of scheduling and synthesizing distributed control programs for a batch production plant. We use a timed automata model of the batch plant and the verification tool UPPAAL to solve the scheduling problem. The plant model aims at faithfully reflecting the level of abstraction required for synthesizing control programs from generated timed traces. Therefore it quickly becomes too detailed and complicated for automatic synthesis. To solve this problem we present a general way of adding guidance to a model by augmenting it with additional guidance variables and decorating the transitions with extra guards. Applying this technique have made synthesis of control programs feasible for a plant producing as many as 60 batches. In comparison, we could only handle plants producing two batches without using guides. The synthesized control programs have been executed in a physical plant. This proved useful in validating the plant model and in finding some modeling errors.