Modular Verification Meets xDSL Dynamics

The OBP2 infra-structure provides advanced tools to debug, simulate and model-check your DSL without relying on transformations.

Overview

OBP (initially Observer Based Prover) is a formal verification environment for systems, designed at ENSTA Bretagne, originally designed around the Fiacre specification language and a context-driven verification methodology. Since 2015, it has been re-architected to become a flexible software framework used not only for model-checking verification but also for animation, model debugging, and execution monitoring on real targets.

Main Characteristics:

  • Extensibility of the Verification Engine: OBP enables seamless integration of domain-specific formalisms such as SDL, BPMN, AnimUML, EMI-UML, TLA+, and Fiacre. This flexibility allows users to adapt OBP to various modeling needs.

  • Integration of Domain-Specific Omniscient Debugging with Model-Checking: This feature bridges the gap between early model diagnosis and formal verification, providing a more comprehensive verification process.

  • Capacity to Decompose the Verification Problem: Based on the Context-aware Verification approach, OBP effectively addresses scalability issues inherent in industrial-scale verification by breaking down complex verification tasks into manageable components.

  • Language Independent Property Specifications: OBP utilizes the GPSL formalism to allow for property specifications that are independent of the underlying modeling language, enhancing the versatility of the verification process.

The analysis engine of OBP operates independently of the formalism, allowing the integration of new modeling languages while being used in various industrial and scientific projects. The tool has been integrated into commercial products for verification purposes, including PragmaDEV PROCESS, a BPMN business process modeling tool, and PragmaDEV Studio, a modeling tool based on SDL.

OBP is open-source software (MIT License) that has generated significant results in academic research and has been involved in collaborative projects, resulting in numerous theses and publications.