PragmaDev Studio V6.1 Features OBP Model Checker

By Chad Cox

Production Editor

Embedded Computing Design

June 09, 2026

News

PragmaDev Studio V6.1 Features OBP Model Checker
Image Credit: PragmaDev

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.

Chad Cox is the Production Editor at Embedded Computing Design. His responsibilities are centered around content creation, writing and editing, and article research and development. Chad covers industry news and events and is known to interact with various industrial leaders via on-premise visits and online interviews. He is responsible for the digital footprint and dissemination of news via social media posts, advertising creation and the production of newsletters including the Embedded Computing Design’s Daily.

He is well versed in many facets of industrial computing including Edge AI, IoT, Processing, Security, Open Source, and more.

Chad graduated from the University of Cincinnati with a B.A. in Cultural and Analytical Literature and holds a master’s in education.

More from Chad

Categories
Debug & Test