process

PragmaDev released the version V6.0 of PragmaDev Studio, a SDL modeling tool, which uses OBP2 for formal verification.

PragmaDev STUDIO is the best SDL modeling tool for the specification and the design of safe communicating software, cristalizing more than 20 years of industrial experience around the SDL-RT standard. Besides improved standard compliance through the support of the new SDL-RT Broadcast feature, the new version of STUDIO integrates OBP2 verification engine as its primary backend for formal verification.

Property Verification

The key characteristic of OBP2 verification engine is that it is not dependent on a specification language. But it relies on a third party executor to execute the model. In PragmaDev Studio V6 OBP2 is interacting with PragmaDev SDL executor to query the semantics. OBP2 does not actually know anything about the model it is exploring. The same principle applies for property verification, complex temporal properties are composed of local atomic proposition. These atomic propositions enable establishing a dialog between the formal verification engine and the STUDIO V6 SDL semantics, which drives the analysis of temporal logic properties. This decoupled, API-based architecture of the OBP2 tool renders it particularly suited for integration with existing complex execution engines. overview

To guide the verification efforts, PragmaDEV STUDIO V6 offers a number of state-space reduction axes, such as constrained message parameters and variable hiding.

Further informations

PragmaDev Studio is free for small projects and education. For more informations do not hesitate to contact PragmaDev