Model Checker Aided Design of a Controller for a Wafer Scanner

M. Hendriks, N.J.M. Nieuwelaar, van den, F.W. Vaandrager

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

12 Citaten (Scopus)


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.
Originele taal-2Engels
Pagina's (van-tot)633-647
TijdschriftInternational Journal on Software Tools for Technology Transfer
Nummer van het tijdschrift6
StatusGepubliceerd - 2006


Duik in de onderzoeksthema's van 'Model Checker Aided Design of a Controller for a Wafer Scanner'. Samen vormen ze een unieke vingerafdruk.

Citeer dit