Guided Synthesis of Control Programs Using UPPAAL
Thomas Hune*, Kim G. Larsen** and Paul Pettersson**
* Aarhus University, DENMARK
** Aalborg University, DENMARK
Abstract
In this paper we address the problem of synthesizing control
programs for a distributed system controlling a batch production plant.
We present a timed automata model of a production plant. This model aims
at faithfully reflecting the level of abstraction required for synthesizing
control programs, 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 decorate transitions with extra guards. Applying this technique
have made synthesis of control programs feasible for a plant producing as many
as 35 batches. In comparison, we could only handle plants producing two
batches without using guides. The synthesized control programs were executed
in the plant. By doing so we found and corrected some errors in the model.
Keywords:
real-time verification, guided model-checking,
scheduling, program synthesis, distributed systems.