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

T. Margaria (Editor), Anton J. Wijs, M. Massink (Editor), Jan Cornelis van de Pol, Elena M. Bortnik

    Research output: Contribution to journalArticleAcademicpeer-review

    4 Citations (Scopus)
    42 Downloads (Pure)

    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.
    Original languageUndefined
    Article number10.1007/s10009-009-0110-9
    Pages (from-to)375-392
    Number of pages18
    JournalInternational journal on software tools for technology transfer
    Volume11
    Issue number5
    DOIs
    Publication statusPublished - 19 Mar 2009

    Keywords

    • EWI-15882
    • FMT-MC: MODEL CHECKING
    • Scheduling
    • METIS-263973
    • IR-67846
    • FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

    Cite this