A dedicated verification approach for scheduling in complex manufacturing machines
van den Njm Barend Nieuwelaar, Mmh Martin Driessen, Jan Friso Groote · TU/e Research Portal · 2004
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.