Chiron User Interface with Decomposed Dispatcher
2 artists, 2 events

DESCRIPTION

In this sample Chiron Interface, there are two artists and two events. The first artist begins by registering for both events, and the second artist registers for the first, but not the second. After this, for an undertermined period, the dispatcher receives events and passes them along to the appropriate artist or artists. Then both artists unregister for each of the events for which they have registered, and the program terminates.

SOURCE CODE

• Ada
• SEDL
• Native Promela
• Ada source code modified for FLAVERS

PROPERTIES

• 0: The system does not deadlock
• 1: Artists register and unregister properly
• 2: Dispatcher notifies before receiving again
• 3: Dispatcher notifies only after receiving
• 4: Dispatcher notifies of what was received
• 5: Dispatcher does not block if no one is registered
• 6: Dispatcher does not notify wrong artists
• 7: Dispatcher notifies artists in order
• 8: Size of registration list does not exceed 2
• 9: All artists unregister before termination

Back to Chiron User Interface

Back to Example Repository for Finite State Verification Tools