وارسی مدل

از ویکی‌پدیا، دانشنامهٔ آزاد
(تغییرمسیر از وارسی مدل نرم‌افزار)

در علوم کامپیوتر، وارسی مدل (به انگلیسی: 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

تفاوت وارسی مدل با تست نرم‌افزار[ویرایش]

در وارسی مدل تمامی برنامه بررسی می‌شود مگر آن که یک عیب پیدا شود. اما در تست نرم‌افزار بر حسب مجموعهٔ ورودی، در آن واحد فقط و فقط یک مسیر اجرا و وارسی می‌شود.

تست وارسی

منابع[ویرایش]