Scheduling Lacquer Production by Reachability Analysis - A Case Study
| Authors: | Behrmann Gerd, Aalborg University, Denmark
Brinksma Ed, University of Twente, Netherlands
Hendriks Martijn, Radboud University, Netherlands
Mader Angelika, University of Twente, Netherlands |
|---|
| Topic: | 5.1 Manufacturing Plant Control |
|---|
| Session: | Dependable Manufacturing Systems Control I |
|---|
| Keywords: | scheduling, model checking cost optimization, timed automata |
|---|
Abstract
In this paper we describe a case study on lacquer production schedulingthat was performed in the European IST-project AMETIST and was provided byone of the industrial partners. The approach is to derive schedules by means ofreachability analysis: with this technique the search mechanism of model checkers,in our case here Uppaal, is used to find feasible or optimal schedules. Theadvantage of this approach is that the expressiveness of timed automata allowsto model scheduling problems of different kinds, unlike many classical approaches,and the problem class is robust against changes in the parameter setting. To fightthe typical state space explosion problem a number of standard heuristics have tobe used. We discuss the diffculties when modelling an industrial case of this kind,describe the experiments we performed, the heuristics used, and the techniquesapplied.
