• OBP2 meets Logo

    An experimental implementation of the Logo educational programming language bound with OBP2.

  • PragmaDEV Process uses OBP2

    process

    PragmaDev released the version 1.0 of PragmaDev PROCESS, a BPMN process modeling tool, which uses OBP2 for formal process verification.

  • GPSL syntax: LTL & Buchi

    Generic Property Specification Language (GPSL) is the language used by OBP2 for specifying the properties that should be verified during the analysis. Currently it supports Linear Temporal Logic and Buchi Automata specifications.

  • OBP2 Version 0.0.6 is out

    OBP2 is a multi language model-checker

  • TLA+ Debug & Model-Checking

    An experimental integration of the TLA+ runtime with the OBP2 debug and model-checking infrastructure.

  • OBP2 Version 0.0.4 is out

    Plug-OBP alias OBP2 is a LTL model-checker for Fiacre models using the OBP compiler providing much more advanded model-checking capabilities. The new version 0.0.4 is out with tons of new features.

  • GPSL syntax

    Generic Property Specification Language (GPSL) is the language used by OBP2 for specifying the properties that should be verified during the analysis (aka LTL for Plug).

  • Projet DSimulator by Michael Rigaud

    Experimental API-level integration of UML Designer with an UML interpreter.

subscribe via RSS