Property 3: Dispatcher notifies only after receiving

DESCRIPTION

Requirement: Dispatcher does not notify any artist of an event until it receives this event from the ADT.

We will concern ourselves with the verification of this requirement for a particular artist (a1) and a particular event (e1):

Refinement: Dispatcher does not notify any artists of e1 until it receives e1 from the ADT.

SPECIFICATION

• Native SPIN
• INCA-SPIN
• INCA-SMV
• INCA
• FLAVERS

Up to Chiron Original Dispatcher (2 artists, 2 events)

Forward to Property 4

Back to Property 2