Abstract
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.
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 language | English |
|---|---|
| Title of host publication | Electronic proceedings of DSVV'2000 |
| Publisher | Uppsala University |
| Number of pages | 8 |
| Publication status | Published - 22 Mar 2000 |
| Externally published | Yes |
| Event | International Workshop on Distributed System Validation and Verification, DSVV 2000 - Taipei, Taiwan Duration: 10 Apr 2000 → 10 Apr 2000 |
Workshop
| Workshop | International Workshop on Distributed System Validation and Verification, DSVV 2000 |
|---|---|
| Abbreviated title | DSVV |
| Country/Territory | Taiwan |
| City | Taipei |
| Period | 10/04/00 → 10/04/00 |