وارسی مدل
در علوم کامپیوتر، وارسی مدل (به انگلیسی: model checking یا property checking) به این مسئله اشاره دارد که آیا مدل یک سیستم یک نیازمندی خاص را پشتیبانی می‌کند یا خیر. بررسی امکان بروز بن‌بست، مسابقه و حالت‌های خاصی که سیستم را از کار می‌اندازد، وظیفهٔ فرایند وارسی مدل نرم‌افزار است. به‌طور خلاصه، وارسی مدل تکنیکی است برای تأیید صحت عملکرد یک سیستم که دارای حالت‌های محدود(en:Finate-state machine) است. این روش برای اطمینان حاصل کردن از صحت عملکرد نیازمندی‌ها و طراحی یک سیستم بلادرنگ و نهفته به کار می‌رود. این شیوهٔ صحت سنجی، تمامی حالت‌های ممکن سیستم را کاوش می‌کند و کلیهٔ سناریوهای ممکن را به روش نظاممند امتحان می‌کند.
روش‌های وارسی مدل
در وارسی مدل کلیهٔ حالت‌ها و انتقال‌های مدل ریاضی مورد بررسی قرار می‌گیرد. با استفاده از یک روش هوشمندانه با دامنهٔ خاص، می‌توان تمامی حالت‌ها را با کاهش زمان محاسبه طی انجام یک عملیات، بررسی کرد. شیوه‌های پیاده‌سازی شامل شمارش فضای حالت‌ها، شمارش فضای حالت‌های نمادین، تفسیر انتزاعی، شبیه‌سازی نمادین و پالایش انتزاعی است. ویژگی‌هایی که اغلب مورد صحت سنجی قرار می‌گیرند، به صورت منطق‌های زمانی مثل منطق زمانی خطی (LTL) یا منطق محاسبات درختی (CTL) توصیف می‌شوند.
مزایا و کاربردها
- این شیوه به نسبت سایر روش‌ها مثل وارسی اثبات، از سرعت بالایی برخوردار است.
- با استفاده از مثال نقضی که در گزارش وارسی تولید می‌گردد، علت عدم ارضای ویژگی مورد انتظار در سیستم را می‌توان کشف نمود.
- این روش، صحت سنجی پاره‌ای را میسر می‌کند. به بیانی دیگر می‌توان هر ویژگی به‌طور مجزا وارسی گردد.
- در هر مرحله از توسعهٔ تولید نرم‌افزار (طراحی، پیاده‌سازی و…) می‌توان از این روش بهره برد.
- کشف خطاهایی که در الگوریتم‌های پیچیده نظیر پروتکل‌های ارتباطی و الگوریتم‌های جمع‌آوری زباله ممکن است رخ دهند و تشخیص آن‌ها در فاز طراحی مشکل است؛ با استفاده از این روش امکان‌پذیر است.
- از جمله ویژگی‌های سیستمی که در وارسی مدل می‌توان از صحت عملکرد آن‌ها در مرحلهٔ پیاده‌سازی سیستم اطمینان حاصل نمود، عبارتند از:
- کشف بروز بن‌بست در برنامه‌های همروند.
- وارسی مشخصات زمانی؛ برای مثال بررسی بروز بن‌بست بعد از گذشت یک ساعت از راه اندازی مجدد سیستم.
مقایسه ابزارهای وارسی مدل
| نام | وارسی مدل | وارسی معادل | واسط گرافیکی کاربر | دسترسی پذیری | |||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| 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 | |
تفاوت وارسی مدل با تست نرم‌افزار
در وارسی مدل تمامی برنامه بررسی می‌شود مگر آن که یک عیب پیدا شود. اما در تست نرم‌افزار بر حسب مجموعهٔ ورودی، در آن واحد فقط و فقط یک مسیر اجرا و وارسی می‌شود.