Home > Products > PragmaDev Studio V6.0 new features


SDL Model Checking

Following a long collaboration with ENSTA Bretagne research lab, PragmaDev has integrated in its latest release of PragmaDev Studio, ENSTA Bretagne model checker OBP (Observer Based Prover).

Exhaustive simulation

The primary objective of model checking is to explore all possible scenarios in the model. During the exploration it is possible to detect dead locks, unreachable model branches, or verify properties.

A language agnostic checker

The key caracteristic of OBP is that it does not rely on a dedicated language. It relies on a third party executor to execute the model. In our case OBP is interacting with PragmaDev SDL executor to execute the transitions. OBP does not actually know anything about the model it is exploring. It is the same principle with the properties. OBP evaluates complex properties made of atomic properties that are evaluated by the execution engine.

OBP integration architecture

Handling the state space

Communicating systems inherently create a lot of possible cases. This is due to the fact that their designs are based on concurrent state machines. This creates a lot of possible paths of execution. So we have implemented ways to reduce the exploration:
  • Reduce the possible parameter values of the incoming messages as well as the number of messages.
    Message parameters
  • Exclude some internal variables from the global model state.
    Internal variables

Broadcast

PragmaDev Studio now supports the Broadcast feature introduced in the latest version of the SDL standard and the SDL-RT recommendation. Until now, each SDL message (or signal) was received by exactly one agent. If a coordinated response was needed, the signal had to be explicitly duplicated and sent to all its recipients. The latest version of SDL includes a new Broadcast feature. By including the phrase 'to all', the engineer indicates in a direct and natural style that every agent that can receive a signal will receive that signal, thus enabling coordinated action. This is a very common situation in communicating systems so this will definitely simplify a lot of designs.

Before this new feature, the sender had to remember the pids of all the receivers, and loop through all of them:

Broadcast old way

The new broadcast is plain and simple:

Broadcast transition

A broadcast trace:

Broadcast trace


Native 64 bit on Windows

Version 6.0 of PragmaDev Studio is now natively 64 bits on Windows. This will help to handle very large models during simulation or exploration.

64 bit icon