-
PragmaDEV STUDIO V6 uses OBP2 for SDL model verification
PragmaDev released the version V6.0 of PragmaDev Studio, a SDL modeling tool, which uses OBP2 for formal verification.
-
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”.
-
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.
-
OBP2 meets Logo
An experimental implementation of the Logo educational programming language bound with OBP2.
-
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.
-
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
- 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
-
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
- 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.4is 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