Paper Info
Title
Production Scheduling by Reachability Analysis - A Case Study
Abstract
Schedule synthesis based on reachability analysis of timed automata has received attention in the last few years. The main strength of this approach is that the expressiveness of timed automata allows - unlike many classical approaches - the modelling of scheduling problems of very different kinds. Furthermore, the models are robust against changes in the parameter setting and against changes in the problem specification. This paper presents a case study that was provided by Axxom, an industrial partner of the AMETIST project. It consists of a scheduling problem for lacquer production, and is treated with the timedautomata approach. A number of problems have to be addressed for the modelling task: the information transfer from the industrial partner, the derivation of timed automaton model for the case study, and the heuristics that have to be added in order to reduce the search space. We try to isolate the generic problems of modelling for model checking, and suggest solutions that are also applicable for other scheduling cases. Model checking experimentsand solutions are discussed.
Year
DOI
Venue
2005
10.1109/IPDPS.2005.363
IPDPS
Keywords
Field
DocType
information transfer,scheduling problem,search space,production scheduling,timed automaton,model checking
Automata theory,Job shop scheduling,Model checking,Computer science,Parallel computing,Scheduling (production processes),Theoretical computer science,Reachability,Heuristics,Timed automaton,Formal verification,Distributed computing
Conference
ISBN
Citations 
PageRank 
0-7695-2312-9
16
0.91
References 
Authors
7
4
Name
Order
Citations
PageRank
Gerd Behrmann1164881.69
Ed Brinksma21676210.11
Martijn Hendriks325518.36
Angelika Mader419919.44