Skip to Main Content Area
CPS-VO
Contact Support
› Go to login screen
Not a member?
Click here to register!
Forgot username or password?
Verification Tool Library
Home
README
Search for Tools
Browse Tool Library
Members
Tutorials
Tutorial - SpaceEx
Files
CPS-VO
»
CPS Tools and Design Studios
»
Verification Tool Library
» OWN LANGUAGE
Own language
wikipage
CADP
Submitted by hgaravel on Thu, 08/16/2018 - 7:29pm
Validation and Verification
Tool
Contact the author
Free
C++
Own interface
Own language
Linux
Mac OS X
Solaris
Windows
Circuits
Continuous-time Markov chains
Discrete-Time Systems
Nested-Unit Petri nets
Network of timed automata
Process calculus language: FSP
Process calculus language: LNT
Process calculus language: LOTOS
Abstractions
Bisimulation minimization
Boolean Equation Systems
Branching-Time Temporal Logics
Breadth First Search Analysis
Compositional verification
Depth-first Search Algorithms
Description/Modeling Language
Distributed model checking
Labelled Transition Systems
Mu-Calculus
On-the-fly model checking
Parallel Composition
Parameterized Boolean Equation Systems
Probabilities on paths
Value-passing Mu-Calculus
Guaranteed to terminate
Not guaranteed to terminate
Bisimulation generation
Description/modeling language
Model checking
Modeling
Probabilistic model checking
Reachability analysis
Simulation
Statistical model checking
Visual checking
wikipage
HyTech
Submitted by akarns on Mon, 05/08/2017 - 11:24am
Validation and Verification
Tool
Free
Own language
Linux
Windows
Linear Hybrid Systems
Clock Translation
Linear Phase Portrait Approximation
Parallel Composition
Parametric Analysis
Not guaranteed to terminate
Model checking
wikipage
Open-Kronos
Submitted by akarns on Mon, 05/08/2017 - 11:14am
Validation and Verification
Tool
Contact the author
Own language
Timed Automata
Depth-first Search Algorithms
On-the-fly model checking
Guaranteed to terminate
Model checking
wikipage
Charon
Submitted by akarns on Mon, 05/08/2017 - 11:04am
Validation and Verification
Tool
Free
Own interface
Own language
Nonlinear hybrid systems
Agent and Mode Architecture
Guaranteed to terminate
Description/modeling language
wikipage
SpeeDI
Submitted by akarns on Mon, 05/08/2017 - 10:51am
Validation and Verification
Tool
Free
Own interface
Own language
Linux
Mac OS X
Windows
Polygonal Hybrid Systems
Simple Planar Differential Inclusions
Guaranteed to terminate
Model checking
wikipage
C2E2
Submitted by akarns on Mon, 05/08/2017 - 10:37am
Validation and Verification
Tool
Free
Own interface
Own language
Linux
Nonlinear hybrid systems
On-the-fly Discrepancy Computation
Overapproximations
Reach Tubes
Guaranteed to terminate
Model checking
wikipage
UPPAAL STRATEGO
Submitted by akarns on Mon, 05/08/2017 - 10:14am
Validation and Verification
Tool
Free
Model editor integrated
Own language
Linux
Windows
Priced timed automata
Stochastic timed automata
Statistical techniques
Timed automata abstractions
Guaranteed to terminate
wikipage
UPPAAL CORA
Submitted by akarns on Mon, 05/08/2017 - 10:13am
Validation and Verification
Tool
Free
Model editor integrated
Own language
Linux
Mac OS X
Windows
Linear priced timed automata
Timed automata abstractions
Guaranteed to terminate
Cost optimal reachability analysis
wikipage
UPAAL SMC
Submitted by akarns on Mon, 05/08/2017 - 10:12am
Validation and Verification
Tool
Free
Model editor integrated
Own language
Linux
Mac OS X
Windows
Priced timed automata
Statistical techniques
Timed automata abstractions
Guaranteed to terminate
Statistical model checking
wikipage
UPPAAL Times Tool
Submitted by akarns on Mon, 05/08/2017 - 10:11am
Validation and Verification
Tool
Free
Model editor integrated
Own language
Linux
Mac OS X
Windows
Network of timed automata extended with tasks
Timed automata abstractions
Guaranteed to terminate
Schedulability analysis
Synthesis
1
2
next ›
last »
