11 ژانویه 2021توسط استیو کرانگ ، دانشگاه میشیگان
گروهی از محققان U-M با استفاده از اثبات ریاضی نشان می دهند که نرم افزار از مشخصات لازم برای اجرای ایمن و صحیح و بدون نیاز به آزمایش سنتی برخوردار است. بر اساس عقل سلیم وقتی نرم افزار می نویسید ، کار خود را بررسی می کنید. آزمایش یک راه حل انتقال از بین تمام ابزارهای دیگری است که ما در طول تاریخ مهندسی انجام داده ایم و این یک سنگ بنای طراحی نرم افزار با کیفیت است. و با این وجود ، به عنوان یک رویکرد مستقل ، امکان آزمایش وجود ندارد . این کار زمان بر است ، کار و منابع زیادی را می طلبد ، و مهمتر از همه انجام آن بسیار دشوار است ، و نرم افزارهای مستقر در همه جا را را مستعد ورودی ها و رفتارهای غیر منتظره می کند.
در واقع ، بیشتر نرم افزارهای مورد استفاده امروزه به قدری پیچیده هستند که آزمایش کامل آن عملاً غیرممکن است.
باریس کاسیکچی ، استادیار دانشگاه توضیح می دهد: “انجام آزمایش های کامل که تمام رفتارهای برنامه های بزرگ را پوشش می دهد ، میلیاردها و میلیارد ها سال به طول می انجامد و اگر موارد خاصی را کنار بگذارید ، اشکالات می توانند وارد کار شوند.
اما بسیاری از سیستم های مهم تا حد زیادی به آزمایش اطمینان می کنند تا از ایمنی و قابل اطمینان بودن آنها اطمینان حاصل کنند .
پروفسور کرم ساکالا می گوید: “ما با نرم افزار بگونه ای بد بازی می کنیم.” “در حال حاضر ، اکثر نرم افزارهایی که ما استفاده می کنیم شکننده هستند و در برخی موارد شکسته می شوند.”
محققانی مانند کاسیکچی و ساکالا گزینه جایگزین هوشمندانه تری را تصور می کنند. به جای اینکه انسان ها ، با تمام محدودیت های تخیل ما ، موارد آزمایشی ارائه دهند ، چرا اجازه نمی دهیم که ریاضیات این وزنه را بلند کرده و کاری را انجام دهند؟ برای راستی آزمایی رسمی ، ابزاری برای اثبات صحیح بودن و قابل اعتماد بودن یک برنامه یا الگوریتم با تمام ظرافت های اثبات منطقی را وارد کنید.
استادیار مانوس کاپریتسوس توضیح می دهد: “تأیید رسمی در اینجا یک گزینه است.” “من قصد ندارم تمام ورودی ها و خروجی های احتمالی را امتحان كنم ؛ من با تبدیل برنامه خود به یك سری فرمول های منطقی ، اثبات می كنم كه خصوصیاتی كه مشخص می كنم در پایان از برنامه من نگهداری می كند.”
این ویژگی که مشخصات نامیده می شود ، برای توصیف نحوه رفتار برنامه طراحی شده است. اساساً ، یک برنامه نویس باید بتواند توصیف کند که خروجی های مختلف یک برنامه چگونه است. ساکالا می گوید: “داشتن یک سیستم ضد خطا که شما آن را توسعه می دهید ، آن را به طور خودکار بررسی می کنید و یک گواهی صحت می گیرید ،” این همان چیزی است که به شما اطمینان می دهد که می توانید بدون مشکل برنامه را مستقر کنید.
یک سوال متداول در مورد راستی آزمایی رسمی این است که چرا فقط در همه موارد استفاده نمی شود ، اگر قرار باشد اینقدردامنه باز باشد. متأسفانه تست مطمئناً زمان بر است و نوشتن کد یا الگوریتم معمولاً در آن قسمت حتی دلیل در مورد همه قطعات به هر حال بدتر است .
