-
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.
-
ONEWAY Project
The P4S Team of Lab-STICC & ENSTA Bretagne are proud to be a partner of the OneWay project, led by Airbus and supported by DGAC (the French Civil Aviation Authority), which aim to ensure digital continuity in the aeronautical sector. OBP2 plays an important role in the verification of the Product Development Plans expressed in BPMN.
-
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.
-
Lancement Projet Ker-SEVECO
Kereval, Mobility Tech Green et l’ENSTA Bretagne démarrent un projet pour améliorer la cybersécurité des véhicules connectés.
-
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
-
AEFD Debug & Model-Checking
Integration of an AEFD runtime with the OBP2 debug and model-checking infrastructure.
-
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.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