iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/s10009-009-0110-9
Solving scheduling problems by untimed model checking | International Journal on Software Tools for Technology Transfer Skip to main content
Springer Nature Link
Log in

Solving scheduling problems by untimed model checking

The clinical chemical analyser case study

  • Regular Paper
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

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 μCRL, 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abdeddaïm, Y., Asarin, E., Maler, O.: On optimal scheduling under uncertainty. In: Proceedings of TACAS 2003. LNCS, vol. 2619, pp. 240–253. Springer, Berlin (2003)

  2. Abdeddaïm Y., Asarin E., Maler O.: scheduling with timed automata. Theor. Comput. Sci. 354(2), 272–300 (2006)

    Article  MATH  Google Scholar 

  3. Abdeddaïm, Y., Kerbaa, A., Maler, O.: Task graph scheduling using timed automata. In: Proceedings of FMPPTA 2003 (2003)

  4. Abdeddaïm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Proceedings of TACAS 2002. LNCS, vol. 2280, pp. 113–126. Springer, Berlin (2002)

  5. Badban B., Fokkink W.J., Groote J.F., Pang J., van de Pol J.C.: Verifying a sliding window protocol in μCRL and PVS. Formal Aspects Comput. 17(3), 342–388 (2005)

    Article  MATH  Google Scholar 

  6. Baeten J.C.M., Middelburg C.A.: Process Algebra with Timing. EATCS Monograph. Springer, Berlin (2002)

    Google Scholar 

  7. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Proceedings of SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Berlin (2004)

  8. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T.: Efficient guiding towards cost-optimality in Uppaal. In: Proceedings of TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Berlin (2001)

  9. Behrmann G., Larsen K.G., Rasmussen J.I.: Optimal scheduling using priced timed automata. SIGMETRICS Perform. Eval. Rev. 32(4), 34–40 (2005)

    Article  Google Scholar 

  10. Bergstra J.A., Klop J.W.: Process algebra for synchronous communication. Inform. Control 60(1–3), 109–137 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  11. Bisiani, R.: Beam search. In: Encyclopedia of Artificial Intelligence, pp. 1467–1568. Wiley, New York (1992)

  12. Blom, S.C.C., Calamé, J.R., Lisser, B., Orzan, S., Pang, J., van de Pol, J.C., Torabi Dashti, M., Wijs, A.J.: Distributed analysis with μCRL: a compendium of case studies. In: Proceedings of TACAS 2007. LNCS, vol. 4424, pp. 683–689. Springer, Berlin (2007)

  13. Blom, S.C.C., Fokkink, W.J., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.C.: μCRL: A toolset for analysing algebraic specifications. In: Proceedings of CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Berlin (2001)

  14. Blom, S.C.C., Ioustinova, N., Sidorova, N.: Timed verification with μCRL. In: Proceedings of PSI 2003. LNCS, vol. 2890, pp. 178–192. Springer, Berlin (2003)

  15. Blom, S.C.C., van Langevelde, I., Lisser, B.: Compressed and distributed file formats for labeled transition systems. In: Proceedings of PDMC 2003. ENTCS, vol. 89. Elsevier, Amsterdam (2003)

  16. Blom S.C.C., Orzan S.: Distributed state space minimization. Int. J. Softw. Tools. Technol. Transf. 7(3), 280–291 (2005)

    Article  Google Scholar 

  17. Bolognesi T., Brinksma E.: Introduction to the ISO specification language LOTOS. Comput. Netw 14(1), 25–59 (1987)

    Article  Google Scholar 

  18. Bozga, M., Kerbaa, A., Maler, O.: Scheduling acyclic branching programs on parallel machines. In: Proceedings of RTSS 2004, pp. 208–215. IEEE Computer Society Press, Washington, DC (2004)

  19. Brucker P., Jurisch B., Sievers B.: A branch and bound algorithm for the job-shop scheduling problem. Discrete Appl. Math. 49(6), 107–127 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  20. Della Croce F., T’kindt V.: A recovering beam search algorithm for the one-machine dynamic total completion time scheduling problem. J. Oper. Res. Soc. 53(11), 1275–1280 (2002)

    Article  MATH  Google Scholar 

  21. Dierks, H., Behrmann, G., Larsen, K.G.: Solving planning problems using real-time model checking (translating PDDL3 into timed automata). In: Proceedings of Workshop on Planning via Model Checking 2002, pp. 30–39 (2002)

  22. Dijkstra E.W.: A note on two problems in connection with graphs. Numer. Math. 1, 269–271 (1959)

    Article  MATH  MathSciNet  Google Scholar 

  23. Edelkamp S.: Taming numbers and duration in the model checking integrated planning system. J. Artif. Intell. Res. 20, 195–238 (2003)

    MATH  Google Scholar 

  24. Fehnker, A.: Citius, vilius, melius: guiding and cost-optimality in model checking. PhD thesis, Radboud University of Nijmegen (2002)

  25. Fox, M.S.: Constraint-Directed Search: A Case Study Of Job-Shop Scheduling. PhD thesis, Carnegie-Mellon University, Pittsburgh (1983)

  26. Garavel, H., Lang, F., Mateescu, R.: An overview of Cadp 2001. In: European Association for Software Science and Technology (EASST) Newsletter, vol. 4, pp. 13–24 (2002)

  27. Groote, J.F., Monin, F., van de Pol, J.C.: Checking verifications of protocols and distributed systems by computer. In: Proceedings of CONCUR 1998. LNCS, vol. 1466, pp. 629–655. Springer, Berlin (1998)

  28. Groote, J.F., Ponse, A.: The Syntax and Semantics of μCRL. In: Proceedings of ACP 1994, Workshops in Computing Series, pp. 26–62. Springer, Berlin (1995)

  29. Groote, J.F., Reniers, M.A.: Algebraic Process Verification. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, chap. 17, pp. 1151–1208. Elsevier, Amsterdam (2001)

  30. Hammer, M., Weber, M.: “to Store or Not to Store” reloaded: reclaiming memory on demand. In: Proceedings of FMICS 2006. LNCS, vol. 4346, pp. 51–66. Springer, Berlin (2006)

  31. Hesen P.M.C.: Design of the Clinical Chemical Analyzer. Technical report. Stan Ackermans Institute, Eindhoven (2000)

    Google Scholar 

  32. Holzmann G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)

    Google Scholar 

  33. Ioustinova, N.: Abstractions and Static Analysis for Verifying Reactive Systems. PhD thesis, Vrije Universiteit Amsterdam (2004)

  34. Kozen D.: Results on the propositional μ-calculus. Theor. Comput. Sci. 27(3), 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  35. Kumar, V.: Branch-and-bound search. In: Shapiro, S. (ed.) Encyclopedia of Artificial Intelligence, pp. 1468–1472. Wiley, New York (1992)

  36. Larsen, K.G.: Resource-efficient scheduling for real time systems. In: Proceedings of EMSOFT 2003. LNCS, vol. 2855, pp. 16–19 (2003)

  37. Lawler, E., Lenstra, J.K., Rinnooy Kan, A., Shmoys, D. (eds.): The Traveling Salesman Problem. Wiley, New York (1985)

    MATH  Google Scholar 

  38. Loeckx J., Ehrich H.-D., Wolf M.: Specification of Abstract Data Types. Wiley, New York (1996)

    MATH  Google Scholar 

  39. Lowerre, B.T.: The HARPY Speech Recognition System. PhD thesis, Carnegie-Mellon University, Pittsburgh (1976)

  40. Luttik, S.P.: Choice Quantification in Process Algebra. PhD thesis, University of Amsterdam (2002)

  41. Mateescu R., Sighireanu M.: Efficient On-the-fly model-checking for regular alternation-free Mu-calculus. Sci. Comput. Program. 46(3), 255–281 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  42. Niebert, P., Tripakis, S., Yovine, S.: Minimum-time reachability for timed automata. In: Proceedings of MED 2000. IEEE Computer Society Press, Washington, DC (2000)

  43. Owre, S., Rushby, J.M., Shankar, N.: PVS: a Prototype Verification System. In: Proceedings of CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Berlin (1992)

  44. Pinedo M.: Scheduling: theory, algorithms, and systems. Prentice-Hall, Englewood Cliffs (1995)

    MATH  Google Scholar 

  45. Pnueli A.: The temporal semantics of concurrent programs. Theor. Comput. Sci. 13(1), 45–60 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  46. Rasmussen, J.I., Larsen, K.G., Subramani, K.: Resource-optimal scheduling using priced timed automata. In: Proceedings of TACAS 2004. LNCS, vol. 2988, pp. 220–235. Springer, Berlin (2004)

  47. Rubin, S.: The ARGOS image understanding system. PhD thesis, Carnegie-Mellon University, Pittsburgh (1978)

  48. Russell S., Norvig P.: Artificial intelligence: A modern approach. Prentice-Hall, Englewood Cliffs (1995)

    MATH  Google Scholar 

  49. Ruys, T.C.: Optimal scheduling using Branch-and-Bound with SPIN 4.0. In: Proceedings of SPIN 2003. LNCS, vol. 2648, pp. 1–17. Springer, Berlin (2003)

  50. Sabuncuoglu I., Bayiz M.: Job shop scheduling with beam search. Eur. J. Oper. Res. 118(2), 390–412 (1999)

    Article  MATH  Google Scholar 

  51. Si Ow P., Morton E.T.: Filtered beam search in scheduling. Int. J. Prod. Res. 26(1), 35–62 (1988)

    Article  Google Scholar 

  52. Si Ow P., Morton E.T.: The single machine early/tardy problem. Manage. Sci. 35(2), 177–191 (1989)

    Article  MATH  Google Scholar 

  53. Si Ow P., Smith S.F.: Viewing scheduling as an opportunistic problem-solving process. Ann. Oper. Res. 12(1-4), 85–108 (1988)

    Google Scholar 

  54. Spronk, W.P.C.: Throughput analysis of a clinical chemical analyzer. Master’s thesis, Technical University of Eindhoven (1999)

  55. Torabi Dashti, M., Wijs, A.J.: Pruning state spaces with extended beam search. In: Proceedings of ATVA 2007. LNCS, vol. 4762, pp. 543–552. Springer, Berlin (2007)

  56. Valente, J.M.S., Alves, R.A.F.S.: Beam search algorithms for the single machine total weighted tardiness scheduling problem with sequence-dependent setups. Working Paper 186, Faculdade de Economia do Porto (2005)

  57. Valente J.M.S., Alves R.A.F.S.: Filtered and recovering beam search algorithms for the early/tardy scheduling problem with no idle time. Comput. Ind. Eng. 48(2), 363–375 (2005)

    Article  Google Scholar 

  58. Veloso, M.M., Pérez, M.A., Carbonell, J.G.: Nonlinear planning with parallel resource allocation. In: Proceedings Innovative Approaches to Planning, Scheduling and Control, pp. 207–212 (1991)

  59. Vervoort, J.: Model of a Chemical Analyzer. WPA Report 420216, Technical University of Eindhoven, Eindhoven (1999)

  60. Weber, S.: Design of Real-Time Supervisory Control Systems. PhD thesis, Technical University of Eindhoven, Eindhoven (2003)

  61. Wijs, A.J.: Achieving discrete relative timing with untimed process algebra. In: Proceedings of ICECCS 2007, pp. 35–44. IEEE Computer Society Press, Washington, DC (2007)

  62. Wijs, A.J.: What to do next? Analysing and optimising system behaviour in time. PhD thesis, Vrije Universiteit Amsterdam (2007)

  63. Wijs, A.J., Fokkink, W.J.: From χ t to μCRL: combining performance and functional analysis. In: Proceedings of ICECCS 2005, pp. 184–193. IEEE Computer Society Press, Washington, DC (2005)

  64. Wijs, A.J., Lisser, B.: Distributed extended beam search for quantitative model checking. In: Proceedings of MoChArt 2006. LNAI, vol. 4428, pp. 165–182. Springer, Berlin (2007)

  65. Wijs, A.J., van de Pol, J.C., Bortnik, E.: Solving scheduling problems by untimed model checking—the clinical chemical analyser case study. In: Proceedings of FMICS 2005, pp. 54–61. ACM Press, New York (2005)

  66. Wouters, A.G.: Manual for the μCRL tool set. Technical Report SEN-R0130, CWI (2001)

Download references

Author information

Authors and Affiliations

  1. INRIA/VASY, 655, Avenue de l’Europe, 38330, Montbonnot St. Martin, France

    Anton J. Wijs

  2. Faculty EEMCS, University of Twente, P.O. Box 217, 7500 AE, Enschede, The Netherlands

    Jaco C. van de Pol

  3. Takumi Technology B.V., Marinus van Meelweg 19a, 5657 EN, Eindhoven, The Netherlands

    Elena M. Bortnik

Authors
  1. Anton J. Wijs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jaco C. van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Elena M. Bortnik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Anton J. Wijs.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Wijs, A.J., van de Pol, J.C. & Bortnik, E.M. Solving scheduling problems by untimed model checking. Int J Softw Tools Technol Transfer 11, 375–392 (2009). https://doi.org/10.1007/s10009-009-0110-9

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-009-0110-9

Keywords

Search

Navigation