• Nov 9, 2020

  OBP2 nominated by Systematic Paris Region Deep Tech Ecosystem

  

  OBP2 was nominated by the Hub Open Source of the Systematic Paris Region Deep Tech Ecosystem for the price “Coup de Cœur Académique”.

• Oct 22, 2020

  OBP2 Verifies Partial UML Models

  AnimUML is a web application that can animate partial UML models. It can also verify these models by connecting to OBP2 over a WebSocket.

• 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