Requirement: The system does not deadlock.
Note: This property is actually violated. A
deadlock can occur in the system in the following kind of situation:
a2 has registered for
now has accepted the call to its
a2 then proceeds to call the dispatcher's
unregister_event entry. Suppose at the same time that
the dispatcher task has accepted a call to its
notify_artists entry and is at the point of calling the
notify_client_event entry in
a2. Then the
dispatcher is blocked until
a2 can proceed, and
a2 is blocked until the dispatcher can proceed, and
deadlock has occured.
Each of the four tools below discovers this deadlock.
Up to Chiron Original Dispatcher (2 artists, 2 events)
Forward to Property 1