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.