Guided Synthesis of Control Programs using Uppaal

Thomas Hune, Kim G. Larsen, Paul Pettersson

Research output: Contribution to journalArticleAcademic

21 Downloads (Pure)


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.In modeling the plant, we aim at a level of abstraction which is sufficiently accurate in order that synthesis of control programs from generated timed traces is possible. Consequently, the models quickly become too detailed and complicated for immediate automatic synthesis. In fact, only models of plants producing two batches can be analyzed directly! To overcome this problem, we present a general method allowing the user to guide the model-checker according to heuristically chosen strategies. The guidance is specified by augmenting the model with additional guidance variables and by decorating transitions with extra guards on these. Applying this method have made synthesis of control programs feasible for a plant producing as many as 60 batches.The synthesized control programs have been executed in a physical plant. Besides proving useful in validating the plant model and in finding some modeling errors, we view this final step as the ultimate litmus test of our methodology's ability to generate executable (and executing) code from basic plant models.
Original languageEnglish
Pages (from-to)43-64
Number of pages22
JournalNordic journal of computing
Issue number1
Publication statusPublished - 2001
Externally publishedYes


Dive into the research topics of 'Guided Synthesis of Control Programs using Uppaal'. Together they form a unique fingerprint.

Cite this