Solving scheduling problems by untimed model checking. The clinical chemical analyser case study

Share/Save/Bookmark

Wijs, Anton J. and Pol, Jaco C. van de and Bortnik, Elena M. (2009) Solving scheduling problems by untimed model checking. The clinical chemical analyser case study. International Journal on Software Tools for Technology Transfer (STTT), 11 (5). pp. 375-392. ISSN 1433-2779

[img] PDF
Restricted to UT campus only
: Request a copy
435kB
[img]
Preview
PDF
225kB
Abstract:In this article, we show how scheduling problems can be modelled in untimed process algebra, by using special tick actions. A minimal-cost trace leading to a particular action, is one that minimises the number of tick steps. As a result, we can use any (timed or untimed) model checking tool to find shortest schedules. Instantiating this scheme to muCRL, we profit from a richer specification language than timed model checkers usually offer. Also, we can profit from efficient distributed state space generators. We propose a variant of breadth-first search that visits all states between consecutive tick steps, before moving to the next time slice. We experimented with a sequential and a distributed implementation of this algorithm. In addition, we experimented with beam search, which visits only parts of the search space, to find near-optimal solutions. Our approach is applied to find optimal schedules for test batches of a realistic clinical chemical analyser, which performs several kinds of tests on patient samples.
Item Type:Article
Copyright:© 2009 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/67846
Official URL:http://dx.doi.org/10.1007/s10009-009-0110-9
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 263973