Skip to main content

Optimal Sceduling of Stochastic Production Processes Through Model Checking

  • Conference paper
  • First Online:
  • 1428 Accesses

Abstract

Modelling and subsequently optimising workflow processes has been a key part of efforts to improve efficiency in production and engineering firms since the beginning of the 20th century (Gilbreth & Gilbreth, 1921).

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

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Van der Aalst, WMP, van Dongen, B. F, Herbst, J., Maruster, L., Schimm, G. & Weijters, A. (2003), Workflow mining: a survey of issues and approaches, Data & knowledge engineering 47 (2), 237-267

    Google Scholar 

  • Aziz, A. Singhal, V. Balarin, F. Brayton, R. Sangiovanni-Vincentelli, A. (1995) It usually works: The temporal logic of stochastic systems. In P. Wolper, (ed.), 7th International Conference on Computer Aided Verication (CAV’95), 939: 155-165. Springer

    Google Scholar 

  • Ball, T., Jones, R. (2006). Eds., ser. Lecture Notes in Computer Science, London, UK: Springer-Verlag, 234-248

    Google Scholar 

  • Basu, A., Bensalem, S., Peled, D. & Sifakis, J. (2011). Priority scheduling of distributed systems based on model checking. Formal Methods in System Design 39(3): 229-245

    Google Scholar 

  • Baier, C., Katoen, J.-P. (2008). Principles of Model Checking. Cambridge MA, USA: The MIT Press

    Google Scholar 

  • Christensen, M.M., Haar, S. (2013) Supermarkeder presser brødkæmpe i minus. Børsen newspaper 8/08/2013. 151:12-13

    Google Scholar 

  • Christiansen, D. R., Carbone, M. & Hildebrandt, T. (2011), Formal semantics and implementation of BPMN 2.0 inclusive gateways, in Proc. of the 7th international conference on Web services and formal methods, ser. Web Services and Formal Methods 2010, Berlin, Heidelberg: Springer-Verlag, 146-160

    Google Scholar 

  • Gilbert, C, Bower, J. L. (2002) Disruptive change. When trying harder is part of the problem. Harv Bus Rev. 80(5):94-101

    Google Scholar 

  • Gilbreth, F. B, Gilbreth, L. M. (1921) Process Charts: First steps in finding the one best way to do work. American Society of Mechanical Engineers (ASME)

    Google Scholar 

  • Gröÿer, M., Norman, G., Baier, C. Ciesinski, F., Kwiatkowska, M. & Parker, D. (2006), On reduction criteria for probabilistic reward models, in Proceedings of the 26th international conference on Foundations of Software Technology and Theoretical Computer Science, ser. FSTTCS’06, Berlin, Heidelberg: Springer-Verlag, pp. 309-320

    Google Scholar 

  • Hansson, H., Jonsson, B. (1994), A logic for reasoning about time and reliability, Formal Aspects of Computing, 6(5): 512-535

    Google Scholar 

  • Herbert, L., Sharp, R. (2013a) Optimisation of BPMN business models via model checking. Proc. for ASME 2013 International Design Engineering Technical Conferences and computers and information in Engineering Conference (IDETC/CIE2013)

    Google Scholar 

  • Herbert, L., Sharp, R. (2013b) Precise analysis of probalistic business process model and notation workflows. Journal of Computing and Information Science in Engineering, 13: 2-11

    Google Scholar 

  • Herbert, L., Sharp, R. (2012a) Quantitative analysis of probabilistic (BPMN) workflows. Proc. for ASME 2012 International Design Engineering Technical Conferences and computers and information in Engineering Conference (IDETC/CIE2012)

    Google Scholar 

  • Herbert, L. & Sharp, R. (2012b), Using stochastic model checking to provision complex business services, in High-Assurance Systems Engineering (HASE), IEEE 14th International Symposium, 98-105

    Google Scholar 

  • Kotter, J. P. (1996) Leading Change. Harvard Business Press

    Google Scholar 

  • Kwiatkowska, M. Norman, G. and Parker, D. (2006). Symmetry reduction for probabilistic model checking, in Proc. 18th International Conference on Computer Aided Verification (CAV’06)

    Google Scholar 

  • Kwiatkowska, M., Norman, G. & Parker, D. (2011). PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV’11), vol. 6806 of LNCS, 585-591, Springer

    Google Scholar 

  • Kwiatkowska, M., Parker, D. (2012), Advances in probabilistic model checking’, in Software Safety and Security - Tools for Analysis and Verification, T. Nipkow, O. Grumberg and B. Hauptmann, Eds., ser. NATO Science for Peace and Security Series - D: Information and Communication Security, IOS Press, vol. 33: 126-151

    Google Scholar 

  • Muehlen, M., Recker, J. (2008). How Much Language Is Enough? Theoretical and Practical Use of the Business Process Modeling Notation. Proceedings for CAiSE ‘08 Proceedings of the 20th international conference on Advanced Information Systems Engineering, 465-479

    Google Scholar 

  • Object Management Group (2011) Business process model and notation (BPMN) 2.0. Standards Document formal/2011-01-03. Webpage: http://www.omg.org/spec/BPMN/2.0/

  • Parker, D. (2012). PRISM 4.0 manual, avaliable: http://www.prismmodelchecker.org/mamual

  • Shingo, S. (1981) Study of Toyota Production System from Industrial Engineering Viewpoint. Japan Management Association

    Google Scholar 

  • Vergidis, K., Tiwari, A. & Majeed, B. (2008) Business process analysis and optimization: beyond reengineering., IEEE Transactions on Systems, Man, and Cybernetics, Part C, 38(1), 69–82.

    Google Scholar 

  • White, D. J. (1993), Markov decision processes. John Wiley & Sons

    Google Scholar 

  • Wijs, A. J., Pol, J. C. van de & Bortnik, E. M. (2009). Solving scheduling problems by untimed model checking : the clinical chemical analyser case study. International Journal on Software Tools for Technology Transfer, 11(5), 375-392

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Herbert, L., Hansen, Z.N.L., Sharp, R., Jacobsen, P. (2015). Optimal Sceduling of Stochastic Production Processes Through Model Checking. In: Schabacker, M., Gericke, K., Szélig, N., Vajna, S. (eds) Modelling and Management of Engineering Processes. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44009-4_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-44009-4_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-44008-7

  • Online ISBN: 978-3-662-44009-4

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics