Formal Verification

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.