Model checker aided design of a controller for a wafer scanner

For a case-study of a wafer scanner from the semiconductorindustry it is shown how model checking techniques can be used tocompute (i) a simple yet optimal deadlock avoidance policy, and (ii) aninfinite schedule that optimizes throughput. Deadlock avoidance is studiedbased on a simple finite state model using Smv, and for throughputanalysis a more detailed timed automaton model has been constructedand analyzed using the Uppaal tool. The Smv and Uppaal models areformally related through the notion of a stuttering bisimulation. Theresults were obtained within two weeks, which confirms once more thatmodel checking techniques may help to improve the design process ofrealistic, industrial systems. Methodologically, the case study is interestingsince two models (and in fact also two model checkers) were usedto obtain results that could not have been obtained using only a single