The possibility of deadlock is an undesired property (to say the least) of safety-critical real-time systems. Therefore, a method to verify that a system cannot deadlock, or to detect possible deadlock situations, is of tremendous value. One such method is resource allocation graphs. As stated in Operating System Concepts by Peterson and Silberschatz [PS85], the occurrence of deadlock requires among other things that hold-wait situations exist and a circular chain of such hold-waits must exist. A resource allocation graph attempts to graphically illustrate all the hold-wait situations in a system. In this graph it is possible to search for cases of circular hold-wait.
