Scheduling Lacquer Production by Reachability Analysis -- A Case Study

Gerd Behrmann, Hendrik Brinksma, Martijn Hendriks, Angelika H. Mader

  • 4 Citations

Abstract

In this paper we describe a case study on lacquer production scheduling that was performed in the European IST-project AMETIST and was provided by one of the industrial partners. The approach is to derive schedules by means of reachability analysis: with this technique the search mechanism of model checkers, in our case here Uppaal, is used to find feasible or optimal schedules. The advantage of this approach is that the expressiveness of timed automata allows to model scheduling problems of different kinds, unlike many classical approaches, and the problem class is robust against changes in the parameter setting. To fight the typical state space explosion problem a number of standard heuristics have to be used. We discuss the difficulties when modelling an industrial case of this kind, describe the experiments we performed, the heuristics used, and the techniques applied to allow to optimize costs (storage costs, delay costs, etc.) while searching for schedules.
Original languageUndefined
Place of PublicationEnschede
PublisherDistributed and Embedded Security (DIES)
Number of pages6
StatePublished - Feb 2005

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-05-05
ISSN (Print)1381-3625

Fingerprint

Costs
Heuristics
Modeling
Automata
Experiment

Keywords

  • EWI-5750
  • METIS-248119
  • IR-57011

Cite this

Behrmann, G., Brinksma, H., Hendriks, M., & Mader, A. H. (2005). Scheduling Lacquer Production by Reachability Analysis -- A Case Study. (CTIT Technical Report Series; No. TR-CTIT-05-05). Enschede: Distributed and Embedded Security (DIES).

Behrmann, Gerd; Brinksma, Hendrik; Hendriks, Martijn; Mader, Angelika H. / Scheduling Lacquer Production by Reachability Analysis -- A Case Study.

Enschede : Distributed and Embedded Security (DIES), 2005. 6 p. (CTIT Technical Report Series; No. TR-CTIT-05-05).

Research output: ProfessionalReport

@book{fa2687264bde4e42acce213fa977c30b,
title = "Scheduling Lacquer Production by Reachability Analysis -- A Case Study",
abstract = "In this paper we describe a case study on lacquer production scheduling that was performed in the European IST-project AMETIST and was provided by one of the industrial partners. The approach is to derive schedules by means of reachability analysis: with this technique the search mechanism of model checkers, in our case here Uppaal, is used to find feasible or optimal schedules. The advantage of this approach is that the expressiveness of timed automata allows to model scheduling problems of different kinds, unlike many classical approaches, and the problem class is robust against changes in the parameter setting. To fight the typical state space explosion problem a number of standard heuristics have to be used. We discuss the difficulties when modelling an industrial case of this kind, describe the experiments we performed, the heuristics used, and the techniques applied to allow to optimize costs (storage costs, delay costs, etc.) while searching for schedules.",
keywords = "EWI-5750, METIS-248119, IR-57011",
author = "Gerd Behrmann and Hendrik Brinksma and Martijn Hendriks and Mader, {Angelika H.}",
note = "Imported from CTIT",
year = "2005",
month = "2",
series = "CTIT Technical Report Series",
publisher = "Distributed and Embedded Security (DIES)",
number = "TR-CTIT-05-05",

}

Behrmann, G, Brinksma, H, Hendriks, M & Mader, AH 2005, Scheduling Lacquer Production by Reachability Analysis -- A Case Study. CTIT Technical Report Series, no. TR-CTIT-05-05, Distributed and Embedded Security (DIES), Enschede.

Scheduling Lacquer Production by Reachability Analysis -- A Case Study. / Behrmann, Gerd; Brinksma, Hendrik; Hendriks, Martijn; Mader, Angelika H.

Enschede : Distributed and Embedded Security (DIES), 2005. 6 p. (CTIT Technical Report Series; No. TR-CTIT-05-05).

Research output: ProfessionalReport

TY - BOOK

T1 - Scheduling Lacquer Production by Reachability Analysis -- A Case Study

AU - Behrmann,Gerd

AU - Brinksma,Hendrik

AU - Hendriks,Martijn

AU - Mader,Angelika H.

N1 - Imported from CTIT

PY - 2005/2

Y1 - 2005/2

N2 - In this paper we describe a case study on lacquer production scheduling that was performed in the European IST-project AMETIST and was provided by one of the industrial partners. The approach is to derive schedules by means of reachability analysis: with this technique the search mechanism of model checkers, in our case here Uppaal, is used to find feasible or optimal schedules. The advantage of this approach is that the expressiveness of timed automata allows to model scheduling problems of different kinds, unlike many classical approaches, and the problem class is robust against changes in the parameter setting. To fight the typical state space explosion problem a number of standard heuristics have to be used. We discuss the difficulties when modelling an industrial case of this kind, describe the experiments we performed, the heuristics used, and the techniques applied to allow to optimize costs (storage costs, delay costs, etc.) while searching for schedules.

AB - In this paper we describe a case study on lacquer production scheduling that was performed in the European IST-project AMETIST and was provided by one of the industrial partners. The approach is to derive schedules by means of reachability analysis: with this technique the search mechanism of model checkers, in our case here Uppaal, is used to find feasible or optimal schedules. The advantage of this approach is that the expressiveness of timed automata allows to model scheduling problems of different kinds, unlike many classical approaches, and the problem class is robust against changes in the parameter setting. To fight the typical state space explosion problem a number of standard heuristics have to be used. We discuss the difficulties when modelling an industrial case of this kind, describe the experiments we performed, the heuristics used, and the techniques applied to allow to optimize costs (storage costs, delay costs, etc.) while searching for schedules.

KW - EWI-5750

KW - METIS-248119

KW - IR-57011

M3 - Report

T3 - CTIT Technical Report Series

BT - Scheduling Lacquer Production by Reachability Analysis -- A Case Study

PB - Distributed and Embedded Security (DIES)

ER -

Behrmann G, Brinksma H, Hendriks M, Mader AH. Scheduling Lacquer Production by Reachability Analysis -- A Case Study. Enschede: Distributed and Embedded Security (DIES), 2005. 6 p. (CTIT Technical Report Series; TR-CTIT-05-05).