Next: , Previous: , Up: Defining and Managing Component States   [Contents]

2.3.2 Interface States versus Component States

You can track states in an interface exactly as you can in a component. When defined in an interface, state declarations differ from the component’s only by 1) having no interface-instance prefix, and 2) having no parentheses. Here are the same states as above, but defined instead in the interface:

interface ILED {
  in void turnOn();
  in void turnOff();

  behaviour {
    enum State { Off, On };
    State state = State.Off;
    on turnOn: { state = State.On; }
    on turnOff: { state = State.Off; }

It is important to understand that there are at least two occasions when one might choose to declare and manage state-related enumerations in an interface:

If you define states in both an interface and in a providing component for that interface, Dezyne verification will ignore the interface’s declared states and only compare the component’s function return values with the interface’s specified function return values.

There is no direct connection between states defined in an interface’s behavioural specification and states defined in a providing component’s implemented behaviour. All that matters is that every stimulus applied to a component-implemented interface function returns a response type that matches the interface’s declared response type, i.e. that every trace through the interface matches every trace through the implementing component for events related to just this interface. For example, we will see later that a model function can be defined to return an integer within a fixed range; verification will find any case of a return outside this range, and will display, in the Trace View window, the exact sequence of steps that led to the mismatch.

Debugging a Model: Interface specification versus Implementation

Dezyne verification examines all possible sequences of execution through a provided interface. Verification finds each mismatch between implementation and specification – e.g., return types, missing events, output events, etc – and displays the entire trace of events that led to the mismatch. Thus, you can quickly and inexpensively fix buried logical errors like race conditions and deadlocks even before any source code is generated or written.

Next: , Previous: , Up: Defining and Managing Component States   [Contents]