Modular Verification Meets xDSL Dynamics

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


OBP is a requirement verification environment, developed at ENSTA Bretagne. The main characteristics are:

  • the extensibility of the verification engine, which enables seamless integration of domain specific formalisms like SDL, BPMN, AnimUML, EMI-UML, TLA+, Fiacre;
  • the integration of domain-specific omniscient debugging with model-checking, which bridge the gap between early model diagnosis and formal verification;
  • the capacity to decompose the verification problem, which, based on the Context-aware Verification approach, addresses the scalability issues in the context of industrial scale verification;
  • Language independent property specifications based on the GPSL formalism.