A Dedicated Verification Approach for Scheduling in Complex Manufacturing Machines

Dynamic scheduling of the production in complex industrial manufacturing machines can lead to problems such as, for instance, deadlocks bringing the production to a standstill. An approach to ensure that deadlock is avoided in these highly flexible systems is to investigate all potential schedules. But verification of industrially sized systems by state-space traversal is practically impossible due to combinatoric effects causing state-space explosion. We present an effective approach to overcome this problem. The approach exploits specific characteristics of the systems and properties under consideration. Three situations in which state-space reduction techniques can be applied have been identified, formally defined and implemented in a dedicated checker. Results show that two of the techniques can reduce state-spaces with an exponential factor, and one technique has a linear effect. The application on a number of wafer scanners shows that this approach makes it possible to verify industrially sized systems.