درستی‌یابی صوری
در زمینه سیستم‌های نرم‌افزاری و سخت افزاری درستی‌یابی صوری عبارتست از عمل ثابت کردن صحت یا عدم صحت الگوریتم‌های زیربنایی یک سیستم برحسب مشخصات صوری خاص با استفاده از روش‌های صوری ریاضیاتی. درستی‌یابی صوری می‌تواند در اثبات درستی سیستم‌هایی مثل پروتکل‌های رمزنگاری، مدارهای ترکیبی، مدارهای دیجیتالی با حافظه داخلی و .. راهگشا باشد. درستی‌یابی این سیستم‌ها از طریق اثبات یک نمایش صوری از یک مدل ریاضی انتزاعی سیستم صورت میگیرد. از جمله مؤلفه‌های ریاضی که اغلب در مدلسازی سیستم‌ها مورد استفاده قرار می‌گیرند می‌توان به موارد زیر اشاره کرد: ماشین حالت محدود، شبکه پتری، ماشین خودکار زمانی، ماشین خودکار ترکیبی و جبر پردازه.
راهکارهای درستی‌یابی صوری
یکی از روش‌ها و ساختارهای درستی‌یابی چک کردن مدل است. این روش شامل یک اکتشاف جامع سیستماتیک مدل ریاضی است. البته این روش برای مدل‌های محدود و بعضی مدل‌های غیرمحدودی که مجموعه‌های نامحدود حالت‌های آن قابل نمایش به‌طور محدود (با استفاده از انتزاع یا استفاده از مزیت‌های تقارن) است قابل استفاده می‌باشد. به‌طور معمول این راهکار از طریق کاوش کردن تمامی حالت‌ها و انتقالات بین آنها از طریق تکنیک‌های هوشمند و خاص-دامنه با هدف در نظر گرفتن تمامی گروه‌های حالت‌ها در یک عملیات و کاهش مرتبه زمانی محاسباتی آن از این طریق می‌باشد. .
درستی‌یابی صوری نرم‌افزار
درستی‌یابی صوری برای برنامه‌های نرم‌افزاری از طریق ثابت کردن آنکه برنامه، خصوصیات صوری رفتارش را ارضاء کند انجام می پذیرد. بخش‌های درستی‌یابی صوری عبارتند از درستی‌یابی استنتاجی، تفسیر انتزاعی، اثبات خودکار قضیه، سیستم‌های نوع. درستی یابی صوری زیر شاخه‌ای از تست نرم افزار است و به بررسی رابط کاربری نرم افزار از دید صوردی برای کاربر نهایی می‌پردازد، در این نوع تست به بررسی رویکردهایی برای بهترین نوع ساختار صوری برنامه‌های نرم افزاری پرداخته می‌شود و با توجه به معیارهای بررسی شده درستی یابی صوری بررسی می‌شود.[1]
درستی‌یابی و اعتبارسنجی
درستی‌یابی یکی از جنبه‌های آزمودن میزان تناسب محصول برای هدف مدنظر است. درحالی که اعتبارسنجی این محصول را از جنبه کامل بودن بررسی می‌کند. به‌طور معمول کلیت فرایند آزمودن تحت عنوان V & V شناخته می‌شود.
اعتبارسنجی: آیا نیاز را به‌طور درست متوجه شدیم و کالای درست را می سازیم؟ به‌طور مثال: آیا این کالا نیازهای حقیقی کاربر را برآورده می‌کند؟
درستی‌یابی: آیا همان داریم چیزی را میسازیم که مدنظرمان بود؟ به‌طور مثال آیا کالای ساخته شده با مشخصات پیش گفته شده اش تطابق دارد؟
فرایند درستی‌یابی متشکل از دو بخش ساختاری/ایستا و رفتاری/پویا می‌باشد. به‌طور خاص در مورد محصول نرم‌افزاری، یکی از این جنبه‌ها به بررسی کد پرداخته و دیگری کد اجرایی را برای نمونه‌های ورودی اجرا و سنجش می‌کند. اما اعتبارسنجی تنها به صورت پویا صورت می پذیرد. به‌طور مثال از طریق آزمودن محصول برای کاربران معمول و غیرمعمول و میزان رضایت آنها.
منابع
- مشارکت‌کنندگان ویکی‌پدیا. «Formal verification». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۱۴ ژانویه ۲۰۱۶.
- Software Engineering Practitioners Approach (ویرایش هفتم) (انگلیسی)
- «نسخه آرشیو شده». بایگانی‌شده از اصلی در ۱۳ ژانویه ۲۰۱۷. دریافت‌شده در ۲۶ آوریل ۲۰۱۷.