Simulation

Formal and semi-formal models can be simulated to verify them. Semi-formal models simulation will use code generation to be executed on the host platform, and formal models will use the built-in simulation kernel.

* Semi-formal simulation is based on the selected target simulator semantic that can be a RTOS simulator or a processor simulator (ISS).
* Formal simulation offers full control over the execution of the system from discrete time execution to real time execution, changing states, changing variable values, generating signals, deleting signals and so on.

The model debugger

Internal information is available through the interface:

    * System information
          o List of running processes,
          o List of pending messages,
          o Re-organize the ordering of the pending messages making simulation undeterministic,
    * Handle time
          o View the list of pending timers,
          o Run the system in discrete time,
          o Have a real time system behavior
    * View local variables
    * Watch remote variables
    * Set graphical breakpoints
    * Step graphically in the model

Set breakpoints and step in the modeler

Dynamic graphical traces

The Simulator and the Debugger can generate a graphical execution trace with a detailed view of the behaviour of the system. Key events in the system have a graphical representation such as: internal states modification, message inputs and outputs with structured parameters, timers, process creations or deletions...

An execution trace

MSC Diff

The MSC Diff checks the differences between two scenarios. It is therefore possible to check:

* a system is conform to its requirements,
* a new version of the system still behaves like the older version (non regression testing).

The diff feature can be configured to filter out some elements. The resulting scenario will display common information in black, and differences in blue or red depending from which diagram the symbol comes from.

Compare against another trace or a requirement