Property 6: Dispatcher does not notify wrong artists

DESCRIPTION

Requirement: Dispatcher never gives an event to an artist that is not registered for it.

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

Refinement: Dispatcher never gives event e1 to artist a1 if a1 is not registered for e1.

SPECIFICATION

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

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

Forward to Property 7

Back to Property 5