|
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.
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.
- Exclude some internal variables from the global model state.
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:
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.