در ، به این مسئله اشاره دارد که آیا مدل یک سیستم یک نیازمندی خاص را پشتیبانی می‌کند یا خیر. بررسی امکان بروز ، و حالت‌های خاصی که سیستم را از کار می‌اندازد، وظیفهٔ فرایند وارسی مدل نرم‌افزار است. به‌طور خلاصه، وارسی مدل تکنیکی است برای تائید صحت عملکرد یک سیستم که دارای حالت‌های محدود( ) است. این روش برای اطمینان حاصل کردن از صحت عملکرد نیازمندی‌ها و طراحی یک سیستم بلادرنگ و نهفته به کار می‌رود. این شیوهٔ صحت سنجی، تمامی حالت‌های ممکن سیستم را کاوش می‌کند و کلیهٔ سناریوهای ممکن را به روش نظاممند امتحان می‌کند.
 در وارسی مدل کلیهٔ حالت‌ها و انتقال‌های مورد بررسی قرار می‌گیرد. با استفاده از یک روش هوشمندانه با دامنهٔ خاص، می‌توان تمامی حالت‌ها را با کاهش زمان محاسبه طی انجام یک عملیات، بررسی کرد. شیوه‌های پیاده‌سازی شامل شمارش فضای حالت‌ها، شمارش فضای حالت‌های نمادین، تفسیر انتزاعی، شبیه سازی نمادین و پالایش انتزاعی است. ویژگی‌هایی که اغلب مورد صحت سنجی قرار می‌گیرند، به صورت منطق‌های زمانی مثل منطق زمانی خطی (LTL) یا منطق محاسبات درختی (CTL) توصیف می‌شوند.
 
 
 
 
 
 
 
 در وارسی مدل تمامی برنامه بررسی می‌شود مگر آن که یک عیب پیدا شود. اما در بر حسب مجموعهٔ ورودی، در آن واحد فقط و فقط یک مسیر اجرا و وارسی می‌شود.
{"title": "وارسی مدل", "link": "https://fa.wikipedia.org//w/index.php?title=%D9%88%D8%A7%D8%B1%D8%B3%DB%8C_%D9%85%D8%AF%D9%84&oldid=34533652", "language": "fa"}