Modular Verification of Executable Specification Languages

OBP2 is a specification and 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 UML, BPMN, 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.