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