وارسی مدل
مقایسه ابزارهای وارسی مدل

| نام>  | وارسی مدل> Plain, Probabilistic, Stochastic,... | وارسی مدل> زبان مدل سازی | وارسی مدل> Properties language | وارسی معادل> Supported equivalences | وارسی معادل> Counter example generation | واسط گرافیکی کاربر> GUI | واسط گرافیکی کاربر> Graphical Specification | واسط گرافیکی کاربر> Counter example visualization | دسترسی پذیری> پروانه نرم‌افزار | دسترسی پذیری> زبان برنامه‌نویسی استفاده شده | دسترسی پذیری> پلتفرم/سیستم عامل      |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| APMC | Approximate Probabilistic | Reactive modules | PCTL, PLTL |  | نه | آری | نه | نه | FUSC | C | Unix & related  |
| ARC | Plain | AltaRica | μ-calculus CTL* |  | آری | آری | نه | نه | FUSC | ANSI C | Unix & related  |
| BANDERA | Code analysis | Java | CTL, LTL |  | آری | آری | آری | آری | رایگان | Java | Windows and Unix related  |
| BLAST | Code analysis | C | Monitor automata |  | آری | نه | نه | نه | رایگان | اکمل | Windows and Unix related  |
| CADENCE SMV | Plain | Cadence SMV, SMV, Verilog | CTL, LTL |  | آری | آری | نه | نه | FUSC | ؟ | Windows and Unix related  |
| CADP | Probabilistic | LOTOS, FSP, LOTOS NT | AFMC | SB, WB, BB, OE, STE, WTE, SE, tau*E | آری | آری | آری | آری | FUSC | ؟ | MacOS, Linux, Solaris, Windows  |
| CBMC | Code analysis | C, C++ | Assertions |  | آری | آری | نه | نه | رایگان | C++ | Windows and Unix related  |
| CPAchecker | Code analyses | C | Monitor automata |  | آری | آری | نه | ? | رایگان | Java | Any  |
| CWB-NC | Plain and Timed | CCS, CSP, LOTOS, TCCS | AFMC, CTL, GCTL | SB, WB, me, ME | آری | آری | نه | نه | FUSC | SML of New Jersey | Windows and Unix related  |
| DBRover | Timed | Ada, C, C++, Java, وی‌اچ‌دی‌ال، Verilog | LTL, MTL |  | نه | آری | آری | آری | غیر آزادCommercial use only | ؟ | Windows and Unix related  |
| DiVinE Tool | Plain | DVE input language | LTL |  | آری | آری | نه | آری | رایگان | C/C++ | Unix, Windows  |
| DREAM | Real-time | C++, Timed automata | Monitor automata |  | آری | نه | نه | نه | رایگان | C++ | Windows and Unix related  |
| Edinburgh CWB | Plain | CCS, TCCS , SCCS | μ-calculus | SB, WB, BB, me, ME, OE | آری | نه | نه | نه | FUSC | SML | Windows and Unix related  |
| EmbeddedValidator | Hybrid | Simulink/Stateflow/TargetLink/C | Monitor automata |  | آری | آری | آری | آری | غیر آزادCommercial use only | ؟ | Windows  |
| Expander2 | Hybrid |  | AFMC, CTL | SB, OE | نه | آری | نه | نه | رایگان | هسکل (زبان برنامه‌نویسی) | Unix related  |
| Fc2Tools | Plain | FC2 | ؟ | SB, WB, BB | آری | نه | آری | آری | رایگان | ؟ | Unix related  |
| GEAR | Plain | ؟ | AFMC, CTL, μ-calculus |  | آری | آری | آری | آری | رایگان | Java | Windows and Unix related  |
| ImProve | Plain | Haskell | Assertions |  | آری | نه | نه | نه | رایگان | Haskell | Linux, Windows, Mac-OS  |
| Java Pathfinder | Plain and timed | Java | unknown |  | نه | آری | نه | نه | NOSA | Java | MacOS, Windows, Linux  |
| LLBMC | Code analysis | C (, C++, all languages supported by LLVM) | Assertions |  | آری | نه | نه | نه | FUSC | C++ | Windows and Unix related  |
| LTSA | Plain | FSP | LTL |  | آری | آری | نه | آری | رایگان | ؟ | Windows and Unix related  |
| LTSmin | Plain | Promela, mCRL2, NIPS-VM, DVE Input Language | μ-calculus, LTL, CTL* | SB, BB | آری | نه | نه | نه | رایگان | C | Unix related  |
| MCMAS | Plain, Epistemic | ISPL | CTL, CTLK |  | آری | آری | نه | آری | رایگان | C++ | Unix, Windows, Mac-OS  |
| mCRL2 | Real-time | mCRL2 | mCRL2 mu-calculus | SB, BB, t*E, STE, WTE | آری | آری | نه | آری | رایگان | C++ | MacOS, Linux, Solaris, Windows  |
| MRMC | Real-time, Probabilistic | Plain MC | CSL, CSRL, PCTL , PRCTL | SB | نه | نه | نه | نه | رایگان | C | Windows, Linux, MacOS  |
| NuSMV | Plain | SMV | CTL, LTL, PSL |  | آری | نه | نه | نه | رایگان | C | Unix, Windows, MacOSX  |
| ompca, OpenMP C Analysis | software symbolic simulation with API control | C/C++ programs with OpenMP directives | logic predicates or flexible procedures through API |  | آری | آری | نه | آری | رایگان | C, C++ | Ubuntu Linux, Windows version available soon  |
| PAT | Plain,Real-time,Probabilistic | CSP#, Timed CSP, Probablilistic CSP | LTL, Assertions |  | آری | آری | آری | آری | رایگان | C# | Windows, other OS with Mono  |
| PRISM | Probabilistic | PEPA, PRISM language, Plain MC | CSL, PLTL , PCTL |  | نه | آری | نه | نه | رایگان | C++, Java | Windows, Linux, MacOS  |
| Reactis Tester | Hybrid | Simulink/Stateflow | ؟ |  | نه | آری | آری | نه | غیر آزادCommercial use only | ؟ | Windows, Linux  |
| RED | dense-time, linear hybrid, fully symbolic | communicating timed automata (CTA), linear-hybrid automata (LHA) | TCTL with fairness assumptions, CTA with fairness assumptions | timed simuilation, fair simulation | آری | آری | آری | آری | رایگان | زبان برنامه‌نویسی سی | Ubuntu Linux  |
| SATABS | Code analysis | C, C++ | Assertions |  | آری | آری | نه | نه | رایگان | C++ | Windows and Unix related  |
| SLMC | Plain | pi-calculus | CCL |  | آری | نه | نه | نه | رایگان | اکمل | Windows and Unix related  |
| SPIN | Plain | Promela | LTL |  | آری | آری | نه | آری | FUSC | C, C++ | Windows and Unix related  |
| TAPAAL | Real-time | Timed-Arc Petri Nets, age invariants, inhibitor arcs, transport arcs | TCTL subset |  | نه | آری | آری | آری | رایگان | C++, Java | MacOS, Windows, Linux  |
| TAPAs | Plain | CCSP | CTL, μ-calculus | SB, WB, BB, STE, WTE, me, ME, OE | آری | آری | آری | آری | رایگان | Java | Windows, MacOS and Unix related  |
| UPPAAL | Real-time | Timed automata, C subset | TCTL subset |  | آری | آری | آری | آری | FUSC | C++, Java | MacOS, Windows, Linux  |
| ROMEO | Real-time | Time Petri Nets, stopwatch parametric Petri nets | TCTL subset |  | آری | آری | آری | نه | رایگان | C++, tcl/tk | MacOS, Windows, Linux  |
| TLC | Plain | TLA+, PlusCal | TLA |  | آری | آری | آری | نه | رایگان | Java | Windows, Linux   |