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

از ویکی‌پدیا، دانشنامهٔ آزاد
پرش به: ناوبری، جستجو

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

راهکارهای درستی‌یابی صوری[ویرایش]

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

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

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

درستی‌یابی و اعتبارسنجی[ویرایش]

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

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