Model Checker Aided Design of a Controller for a Wafer Scanner

Frits Vaandrager
Nijmegen Institute for Computing and Information Sciences
Friday, 12 November, 2004 (All day)
NO

I intend to present an overview of some recent work that has has been carried out within the EU IST project AMETIST, in which timed automata technology is applied to solving various scheduling problems.

One case study that I will discuss in more detail was carried out together with Martijn Hendriks (Nijmegen) and Barend van den Nieuwelaar (ASML/TUE). For a design of a new wafer scanner for the semiconductor industry, we show how model checking techniques can be used to compute (i) a simple yet optimal deadlock avoidance policy, and (ii) an infinite schedule that optimizes throughput. 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 two 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 (and in fact also two model checkers) were used to obtain results that could not have been obtained using only a single model (tool).