درستی‌یابی صوری

یکی از روش‌ها و ساختارهای درستی‌یابی چک کردن مدل است. این روش شامل یک اکتشاف جامع سیستماتیک مدل ریاضی است. البته این روش برای مدل‌های محدود و بعضی مدل‌های غیرمحدودی که مجموعه‌های نامحدود حالت‌های آن قابل نمایش به‌طور محدود (با استفاده از انتزاع یا استفاده از مزیت‌های تقارن) است قابل استفاده می‌باشد. به‌طور معمول این راهکار از طریق کاوش کردن تمامی حالت‌ها و انتقالات بین آن‌ها از طریق تکنیک‌های هوشمند و خاص-دامنه با هدف در نظر گرفتن تمامی گروه‌های حالت‌ها در یک عملیات و کاهش مرتبه زمانی محاسباتی آن از این طریق می‌باشد. .

درستی‌یابی صوری برای برنامه‌های نرم‌افزاری از طریق ثابت کردن آنکه برنامه، خصوصیات صوری رفتارش را ارضاء کند انجام می پذیرد. بخش‌های درستی‌یابی صوری عبارتند از درستی‌یابی استنتاجی، تفسیر انتزاعی، اثبات خودکار قضیه، سیستم‌های نوع. درستی یابی صوری زیر شاخه‌ای از تست نرم افزار است و به بررسی رابط کاربری نرم افزار از دید صوری برای کاربر نهایی می‌پردازد، در این نوع تست به بررسی رویکردهایی برای بهترین نوع ساختار صوری برنامه‌های نرم افزاری پرداخته می‌شود و با توجه به معیارهای بررسی شده درستی یابی صوری بررسی می‌شود.

درستی‌یابی یکی از جنبه‌های آزمودن میزان تناسب محصول برای هدف مدنظر است. درحالی که اعتبارسنجی این محصول را از جنبه کامل بودن بررسی می‌کند. به‌طور معمول کلیت فرایند آزمودن تحت عنوان V & V شناخته می‌شود.
اعتبارسنجی: آیا نیاز را به‌طور درست متوجه شدیم و کالای درست را می سازیم؟ به‌طور مثال: آیا این کالا نیازهای حقیقی کاربر را برآورده می‌کند؟
درستی‌یابی: آیا همان داریم چیزی را میسازیم که مدنظرمان بود؟ به‌طور مثال آیا کالای ساخته شده با مشخصات پیش گفته شده اش تطابق دارد؟
فرایند درستی‌یابی متشکل از دو بخش ساختاری/ایستا و رفتاری/پویا می‌باشد. به‌طور خاص در مورد محصول نرم‌افزاری، یکی از این جنبه‌ها به بررسی کد پرداخته و دیگری کد اجرایی را برای نمونه‌های ورودی اجرا و سنجش می‌کند. اما اعتبارسنجی تنها به صورت پویا صورت می پذیرد. به‌طور مثال از طریق آزمودن محصول برای کاربران معمول و غیرمعمول و میزان رضایت آنها.

• Software Engineering Practitioners Approach (ویرایش هفتم) (انگلیسی)