Next: , Previous: , Up: Dezyne   [Contents][Index]

5 Execution Semantics

The semantics of Dezyne derives from implementing message passing as component based ineraction by means of non-reentrant recursive function invocation. The occurrence of an event is mapped onto a (class-member) function call. Every event function implements the recursive procedural execution of all of the side effects, e.g.: actions (event function invocations(, state updates (assignments), and runtime library interactions: tracing, queueing, flushing and context switching (blocking and unblocking).

For each in-event all action statements are executed depth-first. Each out-event is stored in the event queue of the recipient. After the completion of all on imperative statements, just before control is passed back to the caller, a component will flush its own queue of pending out events. If a component was the recipient of an out-event while it was not executing any events, it will also be requested to flush its queue by the sender of the event.

The execution semantics of Dezyne are illustrated using different model examples and their corresponding sequence diagrams. When interpreting the models and their corresponding event sequence traces, keep in mind that the statements of an event are executed atomically in the context of the behavior that implements the event.

When interpreting the event sequence traces remember the following:

  1. in-events are executed from left to right and return right to left.
  2. out-events are executed from right to left; each event is queued before it is flushed and executed.

In the naming of the different examples the terms direct and indirect are used to indicate that execution respectively continues in the same direction of the initial event, or changes direction at least once.

Note: The behavior of every component example in this chapter has been verified to comply with the behavior of all of its interfaces.

Next: Formal Verification, Previous: Getting Started, Up: Dezyne   [Contents][Index]