Making your own SUT

We employ the UPPAAL GUI to specify SUTs. However, the syntax we use is slightly different from the syntax defined by the UPPAAL developers. We support modelling of locations and transitions, where

• the name of every input event has to start with an 'I'. Similarly, every output event has to start with an 'O'. We do not allow synchronizations. So, every event name does not need to end with a '?' or '!', but with a list of parameter values in parentheses, or empty parentheses in case of no parameters,
• every transition can have a guard. We allow tests for equality (==) or inequality (!=) of parameter values, where different tests can be concatenated via '&&' or '||'. At the moment we only allow comparison of Integer values, and
• every transition can have zero or more update statements to update the state variables, e.g. by storing parameter values. Every statement has to end with a semicolon.
• random is a special function used to model fresh output parameters

Currently, Tomte can learn SUTs that can be modeled by extended finite state machines with data parameters, a finite number of state variables over which guards and actions are defined. We restrict operations in these machines to assignments, and guards to just predicates testing for equality. We are not able yet to learn timed systems nor can we infer more complex predicates or operations (for example, increments). As of recent, we can learn systems that generate random output values. We suggest the most recent publication, for an up to date descriptions of these models.

Figure 1 shows an example model of the alternating bit protocol receiver that conforms to our syntax.

Figure 1: Example model of the alternating bit protocol receiver

In addition to modelling the system, we require a number of declarations (added in the 'Declarations' section in UPPAAL), which are

• the constants that appear in the system,
• an enumeration of all state variables in the system, and
• an enumeration of all events in the system.

For the alternating bit protocol receiver model shown above, the declarations are as follows:

  const int zero = 0;
  const int one = 1;

  int vd;
  int vb;
  int expectedBit = 0;

  void IFrame(int d, int b) {
  }

  void IPleaseAck() {
  }

  void OOut(int vd) {
  }

  void OAck(int vb) {
  }

  void ONOK() {
  }

Finally, copy your file to the subfolder 'models'.

Below is an model of a Multi-Login System which uses fresh output values to generate password. Notice the random function used to define the OOK transition, which carries a single fresh output value as parameter.

Fig. 1: SUT Model : Login with fresh output parameters