PragmaDev Studio V6.1 Features OBP Model Checker
June 09, 2026
News
PragmaDev introduced its PragmaDev Studio V6.1 with improvements to model exploration and state space reduction. PragmaDev Studio is employed for model checking and formal verification, allowing developers to analyze complex systems more efficiently than before.
In collaboration with the ENSTA Bretagne research laboratory, PragmaDev integrated the Observer Based Prover (OBP) model checker into PragmaDev Studio V6. OBP avoids the need for a dedicated modeling language and relies instead on an external execution engine to perform model exploration.
According to the press release, OBP interacts directly with PragmaDev SDL execution engine to execute model transitions resulting in OBP remaining entirely independent of the model structure itself. The same applies to property verification (complex properties are decomposed into atomic properties, which are evaluated by the execution engine during exploration).
New Enhanced State Space Reduction Techniques:
- Reducing the range of possible values for complex parameters carried by incoming messages
- Limiting the number of incoming messages considered for each message type
- Automatically identifying internal variables that can be excluded from the global model state without affecting verification results
For more information, visit pragmadev.com/product/newFeatures.html.
