Guided Synthesis of Control Programs Using UPPAAL

T. Hune, Kim Guldstrand Larsen, P. Pettersson

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskning

Abstrakt

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.
OriginalsprogEngelsk
TitelProceedings for International Workshop on Distributed Systems Verification and Validation
RedaktørerTen H. Lai
Publikationsdato2000
Sider15-22
StatusUdgivet - 2000
BegivenhedInternational Workshop on Distributed Systems Verification and Validation - Taipei, Taiwan
Varighed: 10 apr. 200013 apr. 2000

Konference

KonferenceInternational Workshop on Distributed Systems Verification and Validation
LandTaiwan
ByTaipei
Periode10/04/200013/04/2000

    Fingerprint

Citationsformater

Hune, T., Larsen, K. G., & Pettersson, P. (2000). Guided Synthesis of Control Programs Using UPPAAL. I T. H. Lai (red.), Proceedings for International Workshop on Distributed Systems Verification and Validation (s. 15-22)