Guided Synthesis of Control Programs Using UPPAAL

Thomas Hune, Kim G. Larsen, Paul Pettersson

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 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. 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.
Original languageEnglish
Title of host publicationElectronic proceedings of DSVV'2000
PublisherUppsala University
Number of pages8
Publication statusPublished - 22 Mar 2000
Externally publishedYes
EventInternational Workshop on Distributed System Validation and Verification, DSVV 2000 - Taipei, Taiwan
Duration: 10 Apr 200010 Apr 2000


WorkshopInternational Workshop on Distributed System Validation and Verification, DSVV 2000
Abbreviated titleDSVV


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

Cite this