Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Model checker aided design of a controller for a wafer scanner

  • Special Section on Quantitative Analysis of Real-time Embedded Systems
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

For a case-study of a wafer scanner from the semiconductor industry it is shown how model checking techniques can be used to compute (1) a simple yet optimal deadlock avoidance policy, and (2) an infinite schedule that optimizes throughput. in the absence of errors. Deadlock avoidance is studied based on a simple finite state model using Smv, and for throughput analysis a more detailed timed automaton model has been constructed and analyzed using the Uppaal tool. The Smv and Uppaal models are formally related through the notion of a stuttering bisimulation. The results were obtained within 2 weeks, which confirms once more that model checking techniques may help to improve the design process of realistic, industrial systems. Methodologically, the case study is interesting since two models were used to obtain results that could not have been obtained using only a single model.

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. Alur R., Courcoubetis C., Dill D.L. (1993). Model checking in dense real time. Inform. Comput. 104: 2–34

    Article  MathSciNet  Google Scholar 

  2. Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: ICALP’90, pp. 322–335 (1990)

  3. Alur R., Dill D.L. (1994). A theory of timed automata. Theor. Comput. Sci. 126: 183–235

    Article  MathSciNet  Google Scholar 

  4. Behrmann, G., Brinksma, E., Hendriks, M., Mader, A.: Scheduling lacquer production by reachability analysis – a case study. In: Workshop on parallel and distributed real-time systems 2005. IEEE Computer Society Press (2005, to appear)

  5. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: SFM’04, LNCS, vol. 3185, pp. 200–236. Springer, Berlin Heidelberg New York (2004)

  6. Bohnenkamp, H.C., Hermanns, H., Klaren, R., Mader, A., Usenko, Y.S.: Synthesis and stochastic assessment of schedules for lacquer production. In: Proceedings of 1st international conference on quantitative evaluation of systems (QEST 2004), 27-30 September 2004, Enschede, pp. 28–37. IEEE Computer Society (2004)

  7. Braspenning, N.C.W.M.: Scheduling and behavior verification of machines based on task-resource models. Master’s thesis, Department of Mechanical Engineering, Eindhoven University of Technology, The Netherlands (2003)

  8. Browne M.C., Clarke E.M., Grumberg O. (1988). Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1,2): 115–131

    Article  MathSciNet  Google Scholar 

  9. Bryant R.E. (1986). Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8): 677–691

    Google Scholar 

  10. Clarke E.M., Grumberg O., Peled D.A. (2000). Model Checking. The MIT Press, Cambridge

    Google Scholar 

  11. Dijkstra E.W. (1965). Cooperating sequential processes. Technical report. Eindhoven University of Technology, The Netherlands

    Google Scholar 

  12. Fehnker, A.: Scheduling a steel plant with timed automata. In: RTCSA’99. IEEE Computer Society Press (1999)

  13. Gebremichael, B., Vaandrager, F.W.: Control synthesis for a smart card personalization system using symbolic model checking. In: Larsen, K.G., Niebert P. (eds) FORMATS’03, no. 2791 in LNCS, pp. 189–203. Springer, Berlin Heidelberg New York (2004)

  14. Hartonas-Garmhausen, V., Clarke, E.M., Campos, S.: Deadlock prevention in flexible manufacturing systems using symbolic model checking. In: IEEE conference on robotics and automation. vol. 1, pp. 527–532 (1996)

  15. Lawley M., Reveliotis S.A. (2001). Deadlock avoidance for sequential resource allocation systems: hard and easy cases. Int. J. Flex. Manuf. Sys. 13(4): 385–404

    Article  MathSciNet  Google Scholar 

  16. Lawley M., Reveliotis S.A., Ferreira P. (1997). Design guidelines for deadlock handling strategies in flexible manufacturing systems. Int. J. Flex. Manuf. Sys. 9(1): 5–30

    Article  Google Scholar 

  17. McMillan, K.L.: Symbolic model checking. Ph.D. thesis, Carnegie Mellon University (1992)

  18. Murata T. (1989). Petri nets: properties, analysis, and applications. P. IEEE 77(4): 541–580

    Article  Google Scholar 

  19. Niebert, P., Yovine, S.: Computing optimal operation schemes for chemical plants in multi-batch mode. In: HSCC, LNCS, vol. 1790, pp. 338–351. Springer, Berlin Heidelberg New York, (2000)

  20. Park J., Reveliotis S.A. (2001). Deadlock avoidance in sequential resource allocation systems with multiple resource acquisitions and flexible routings. IEEE T. Automat. Contr. 46(10): 1572–1583

    Article  MathSciNet  Google Scholar 

  21. Reveliotis S.A., Lawley M., Ferreira P. (1997). Polynomial-complexity deadlock avoidance policies for sequential resource allocation systems. IEEE T. Automat. Contr. 42(10): 1344–1357

    Article  MathSciNet  Google Scholar 

  22. Stallings, W.: Operating Systems. Prentice-Hall, Englewood Cliffs (1998)

  23. Wang, Y., Wu, Z.: Deadlock avoidance control synthesis in manufacturing systems using model checking. In: IEEE American Control Conference, vol. 2, pp. 1702–1704 (2003)

  24. Yovine S. (1997). Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. 1(1/2): 123–133

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Computing and Information Sciences, Radboud University Nijmegen, Nijmegen, The Netherlands

    Martijn Hendriks & Frits Vaandrager

  2. ASML, Veldhoven, The Netherlands

    Barend van den Nieuwelaar

Authors
  1. Martijn Hendriks
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Barend van den Nieuwelaar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Frits Vaandrager
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martijn Hendriks.

Additional information

Supported by the European Community Project IST-2001-35304 (Ametist), http://ametist.cs.utwente.nl/.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Hendriks, M., van den Nieuwelaar, B. & Vaandrager, F. Model checker aided design of a controller for a wafer scanner. Int J Softw Tools Technol Transfer 8, 633–647 (2006). https://doi.org/10.1007/s10009-006-0025-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-006-0025-7

Keywords

Search

Navigation