Next: Formal Verification, Previous: Getting Started, Up: Dezyne [Contents][Index]
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:
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]