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)
17 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

Margaria, T. (Editor) ; Wijs, Anton J. ; Massink, M. (Editor) ; van de Pol, Jan Cornelis ; Bortnik, Elena M. / Solving scheduling problems by untimed model checking. The clinical chemical analyser case study. In: International journal on software tools for technology transfer. 2009 ; Vol. 11, No. 5. pp. 375-392.
@article{d4714940b5b049f18b7a3de7e57d5b98,
title = "Solving scheduling problems by untimed model checking. The clinical chemical analyser case study",
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.",
keywords = "EWI-15882, FMT-MC: MODEL CHECKING, Scheduling, METIS-263973, IR-67846, FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS",
author = "T. Margaria and Wijs, {Anton J.} and M. Massink and {van de Pol}, {Jan Cornelis} and Bortnik, {Elena M.}",
note = "10.1007/s10009-009-0110-9",
year = "2009",
month = "3",
day = "19",
doi = "10.1007/s10009-009-0110-9",
language = "Undefined",
volume = "11",
pages = "375--392",
journal = "International journal on software tools for technology transfer",
issn = "1433-2779",
publisher = "Springer",
number = "5",

}

Solving scheduling problems by untimed model checking. The clinical chemical analyser case study. / Margaria, T. (Editor); Wijs, Anton J.; Massink, M. (Editor); van de Pol, Jan Cornelis; Bortnik, Elena M.

In: International journal on software tools for technology transfer, Vol. 11, No. 5, 10.1007/s10009-009-0110-9, 19.03.2009, p. 375-392.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

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

AU - Wijs, Anton J.

AU - van de Pol, Jan Cornelis

AU - Bortnik, Elena M.

A2 - Margaria, T.

A2 - Massink, M.

N1 - 10.1007/s10009-009-0110-9

PY - 2009/3/19

Y1 - 2009/3/19

N2 - 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.

AB - 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.

KW - EWI-15882

KW - FMT-MC: MODEL CHECKING

KW - Scheduling

KW - METIS-263973

KW - IR-67846

KW - FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

U2 - 10.1007/s10009-009-0110-9

DO - 10.1007/s10009-009-0110-9

M3 - Article

VL - 11

SP - 375

EP - 392

JO - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

SN - 1433-2779

IS - 5

M1 - 10.1007/s10009-009-0110-9

ER -