• Dec 12, 2019

  OBP2 meets Logo

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

• Nov 15, 2019

  PragmaDEV Process uses OBP2

  

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

• May 9, 2019

  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.

• Dec 10, 2018

  OBP2 Version 0.0.6 is out

  • Download Version 0.0.6

  OBP2 is a multi language model-checker

  • Fiacre models using the OBP compiler
  • TLA models using the tlatools for TLA model compilation
• Oct 7, 2018

  TLA+ Debug & Model-Checking

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

• Apr 16, 2018

  OBP2 Version 0.0.4 is out

  • Download Version 0.0.4

  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.

• Apr 11, 2018

  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).

• Oct 10, 2016

  Projet DSimulator by Michael Rigaud

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

subscribe via RSS