انجمن انفورماتیک ایران انجمن انفورماتیک ایران انجمن انفورماتیک ایران
گزارش کامپیوتر شماره 234, ویژه مرداد و شهریور ماه 96 منتشر شد. چهارشنبه  ٠١/٠٩/١٣٩٦ ساعت ٢٠:١١
 

روش‌های صوری و مهندسی نرم‌افزار سخت‌گير

علیرضا خلیلیان
دانشجوی دکتری نرم افزار
دانشکده مهندسی کامپیوتر، دانشگاه اصفهان
پست الکترونیکی: khalilian@eng.ui.ac.ir

 


 

چکیده
نرم‌افزار هم مانند هر محصول دیگر بشری باید با کیفیت باشد. شاید اگر ویندوز سیستم شخصی شما از کار بیفتد، بجز دو سه دقیقه صبر تا راه‌اندازی مجدد سیستم، هزینه دیگری تحمیل نشود. اما اگر نرم‌افزار پرتودرمانی که اشعه ایکس به بیماری می‌تاباند، خطا داشته باشد، بیمار ممکن است جانش را از دست بدهد. این مقاله راجع به استفاده از روش‌های ریاضی در توسعه نرم‌افزار است که جلوی چنین مشکلاتی را بگیرد. هدف ما صرفاً روشن کردن زمینه مفاهیم موضوع و اهمیت آن است؛ بنابراین از ارائه هر گونه جزئیات فنی و تخصصی اجتناب شده است. مقاله سعی می‌کند با شیوه روایی مطلب را ارائه دهد.

مقدمه
نرم‌افزارهای امروز بسیار بزرگ و پیچیده هستند و پیچیده‌تر هم می‌شوند. افزایش پیچیدگی نرم‌افزار مستقیماً بر کیفیت آن اثر می‌گذارد و تضمین کیفیت دشوارتر می‌گردد. دشواری این فعالیت به‌خاطر اینست که نرم‌افزارها را انسان‌ها تولید می‌کنند و انسان‌ها اشتباه می‌کنند؛ و احتمال اشتباه کردن انسان با افزایش پیچیدگی محصول تولیدی بیشتر می‌گردد. خطای انسان باعث می‌شود نرم‌افزار حاصل معیوب باشد و همیشه و مطابق خواسته برنامه‌سازان کار نکند. در این‌صورت، می‌گوییم نرم‌افزار تولید شده کیفیت پایینی دارد. چون اکثر کارهای روزمره بشر وابستگی شدیدی به نرم‌افزار دارد، کارکرد نادرست نرم‌افزار یا کیفیت پایین آن هم باعث خسارت‌های مالی و هم جانی هنگفت می‌گردد. بنابراین مهندسان نرم‌افزار باید سعی کنند طوری سیستم‌های کامپیوتری و نرم‌افزاری را طراحی کنند که عاری از هر گونه نقص و مشکل باشد.
نقص‌ها گاهی در کارکرد سیستم‌ها هستند و گاهی در خصوصیت‌های غیرکارکردی سیستم دیده می‌شوند. مثلاً با زدن دکمه‌ای در نرم‌افزار، انتظار دارید اطلاعاتی چاپ شود ولی نرم‌افزار ناگهان بسته می‌شود. یا ممکن است موقع گزارش گرفتن در نرم‌افزار، بیش از حد نرم‌افزار تأخیر داشته باشد. اولی نقص کارکردی است و دومی مشکل غیرکارکردی. مشکل غیرکارکردی وقتی است که سیستم رفتار درستی دارد ولی مشکلات دیگری دارد مثل کارایی پایین، امنیت کم و قابلیت نگهداری ضعیف. نقص‌ها گاهی در کارکرد سیستم‌ها هستند و گاهی در خصوصیت‌های غیرکارکردی سیستم دیده می‌شوند. مثلاً با زدن دکمه‌ای در نرم‌افزار، انتظار دارید اطلاعاتی چاپ شود ولی نرم‌افزار ناگهان بسته می‌شود. یا ممکن است موقع گزارش گرفتن در نرم‌افزار، بیش از حد نرم‌افزار تأخیر داشته باشد. اولی نقص کارکردی است و دومی مشکل غیرکارکردی. مشکل غیرکارکردی وقتی است که سیستم رفتار درستی دارد ولی مشکلات دیگری دارد مثل کارایی پایین، امنیت کم و قابلیت نگهداری ضعیف.
کیفیت ناشی از دقت، سخت‌گیری، وضوح و عدم ابهام در مراحل طراحی و پیاده‌سازی است. این ویژگی‌ها در ریاضیات دیده می‌شوند. بنابراین دانشمندان علم کامپیوتر سعی کردند که از ابزار ریاضی مناسب در تولید نرم‌افزار استفاده کنند. این مقاله برخی از جنبه‌های مهم این‌کار را بازگو می‌نماید.
در تولید هر نرم‌افزار ابتدا باید بگوییم چه می‌خواهیم: نیازهای خود را بیان کنیم. سپس نرم‌افزار را طراحی و پیاده‌سازی کنیم و بعد وارسی کنیم که درست ساخته‌ایم یا خیر. در هر سه کار از ریاضی استفاده می‌شود که بر پایه «روش صوری » هدایت می‌شود: بیان ریاضی نیازها.
مقاله در سه بخش بعدی، ابتدا راجع به روش‌های صوری صحبت می‌کند، سپس وارد بخش مهندسی نرم‌افزار سخت‌گیر می‌شود و در نهایت پیرامون رویکرد صحیح به ساخت برای برنامه‌سازی بحث می‌نماید. مقدمه‌ای که در این بخش ذکر شد، عمومی است و هر یک از بخش‌های بعدی نیز به فراخور مطالب اختصاصی‌اش، مقدمه‌ای دارد.


روش‌های صوری
با همه تلاش‌های بشر، مواقع بسیاری می‌بینم که نرم‌افزار مطابق نظر طراح و برنامه‌ساز کار نمی‌کند. در این‌صورت نرم‌افزار معیوب است و کیفیت پایینی دارد. معیوب بودن یعنی نرم‌افزار قابل اعتماد نیست و مشکلات احتمالی آن گاهی پیامدهای سنگینی دارد، باعث سقوط هواپیما، انفجار نیروگاه یا تشعشع بیش از حد پرتو ایکس به بیماران سرطانی می‌شود. همه این موارد یعنی کیفیت پایین نرم‌افزار باعث تحمیل خسارت‌های مالی و جانی سنگین شده است.
یکی از علت‌های کیفیت پایین نرم‌افزار، مستندات مبهم است. همراه با هر نرم‌افزار مستندات بسیاری عرضه می‌شود که راهنمای کاربران، مستندات طراحی و جزئیات نرم‌افزار را تشریح می‌کنند. متأسفانه متنی که به زبان محاوره‌ای طبیعی نوشته می‌شود ممکن است ناقص، ناسازگار یا مبهم باشد. پس هر محصولی که بر پایه چنین مستنداتی تولید شود، در معرض معیوب بودن قرار می‌گیرد. روش‌های صوری، راهی دقیق و نامبهم برای توصیف سیستم‌ها به‌جای متن، عکس و نمودار، جدول و مستندات متنی است.
روش‌های صوری، راهی دقیق و نامبهم برای توصیف سیستم‌ها به‌جای متن، عکس و نمودار، جدول و مستندات متنی است.
روش‌های صوری بر مبنای ریاضی کار می‌کنند تا دقیق‌تر باشند، بهتر درک شوند و بتوانیم در مورد جنبه‌های آن‌ها با اطمینان «استدلال » کنیم. اگرچه استفاده از ریاضی در کل گران است ولی دقت و کیفیتی که به‌دست می‌آید، هزینه‌های کلی طراحی، توسعه، پیاده‌سازی و نگهداری نرم‌افزار را کاهش می‌دهد؛ و مشتریان هم رضایت‌مندی بیشتری دارند. گران بودن ریاضیات یعنی یادگیری آن زمان‌گیر و دشوار است و ابزارهای مرتبط با آن هم پیچیدگی‌های محاسباتی زیادی دارند. روش‌های صوری در بسیاری از جنبه‌های سیستم‌های کامپیوتری مورد استفاده قرار گرفته‌اند: نظریه احتمالات در مدل‌سازی و ارزیابی کارایی سیستم‌های کامپیوتری، استفاده از جبر و حساب رابطه‌ای در پایگاه داده‌ها و استفاده از دستور زبان‌های نابسته به متن نمونه‌های رایج هستند. علاوه بر این‌ها، گونه‌ای از روش‌های صوری هم برای توصیف و طراحی سیستم‌های نرم‌افزاری استفاده می‌شود. هدف این روش‌ها، توصیف خصوصیات حالت و مبتنی بر حالت، نظریه پالایش و ارتقاء است که در همه مراحل توسعه برنامه قابل استفاده است.
از بین انبوه روش‌های صوری، زبان Z یکی از مشهورترین‌هاست که توسط جیم وودکوک و جیم دِیویس در دانشگاه آکسفورد ابداع شد. زبان Z تشکیل می‌شود از یک زبان ریاضی حاوی نظریه مجموعه‌ها و منطق در قالب «حساب مسندات مرتبه اول » به‌همراه سازوکار ساختاربندی. زبان Z در ترکیب با زبان طبیعی محاوره‌ای برای تولید و توصیف رسمی قابل استفاده است و با کمک اثبات قضیه، می‌توان در مورد توصیف‌ها استدلال کرد. همچنین توصیف را می‌توان پالایش کرد تا توصیف دیگری نزدیک به کد نرم‌افزار به‌دست آید. از زبان Z نمی‌توان برای توصیف خصوصیت‌های غیرکارکردی یا رفتار زمان‌دار و هم‌روند استفاده کرد و برای این منظورها زبان‌های دیگری وجود دارند.
زبان Z تأکید بسیاری بر اثبات قضیه دارد. اثبات مانند غلط‌گیری در متن نوشته شده است و بخش ضروری در نوشتن هر توصیف است. توصیف رسمی بدون اثبات، آزمون نشده است. در این‌صورت احتمال ناسازگاری، توصیف‌های اضافی، حذف توصیف‌های ضروری و فرض‌های نامناسب وجود دارد. استدلال در مورد توصیف و ساخت اثبات باعث می‌شود مهندسان مشکلات احتمالی را در مراحل اولیه توسعه سیستم کشف کنند. اثبات در مرحله توصیف نیازمندی‌ها سهم مهمی در کیفیت نرم‌افزار دارد. اثبات در مرحله طراحی نشان می‌دهد طراحی درست است یا خیر و کمک می‌کند پیامدهای ناشی از تغییرها، تکامل و افزوده‌ها را ساده‌تر بررسی و کشف کنیم. اثبات در مرحله پیاده‌سازی تضمین می‌کند کد نوشته شده مطابق توصیف اولیه عمل می‌کند و سهم مهمی در کیفیت نرم‌افزار دارد.
نکته مهم اینست که بدانیم اثبات‌ها در چه موقعیتی باید استفاده شوند. در حال حاضر، وقتی از روش‌های سبک‌وزن استفاده شود و اثبات‌ها در سطح مناسبی از رسمیت ساخته شوند، روش‌های صوری کاملاً در صنعت مقیاس‌پذیر می‌شوند.
یکی از خصوصیت‌های مهم توصیف صوری خوب، انتخاب مناسب سطح «انتزاع » است. اولین نقشه‌ای که برای متروی لندن در سال 1908 عرضه شد، به‌خاطر ارائه جزئیات دقیق پیچ‌ها، مسیرها و تقاطع راه‌ها بسیار پیچیده شده بود و استخراج اطلاعات را سخت می‌کرد. سپس در سال 1933 نقشه دیگری ارائه شد که انتزاعی‌تر بود: این نقشه جدید اتصال ایستگاه‌ها به‌هم و توالی آن‌ها را حفظ کرده بود ولی جزئیات غیرضروری را حذف کرده بود. یعنی دیگر لازم نبود در نقشه پیچیدن مسیر نشان داده شود، صرفاً کافی بود معلوم شود ایستگاه بعدی چیست و این خط مترو با چه خطی در چه نقطه‌ای تلاقی دارد. نقشه جدید در سطح «لازم» از رسمیت ارائه شده بود:

  • انتزاعی: چون صرفاً طرح منطقی را نشان می‌دهد نه واقعیت فیزیکی با همه جزئیات
  • فشرده: چون اندازه‌اش کوچک است تا راحت استفاده شود.
  • کامل: حاوی اطلاعات همه ایستگاه‌ها
  • نامبهم: توضیح معنای همه نمادها با زبان ساده، دقیق و صحیح
  • قابل نگهداری: چون در طی بیش از 70 سال توانسته منعکس کننده تغییرات، افزوده‌ها و حذفی‌ها باشد.
  • قابل درک: چون عموم مردم (کاربران) می‌توانند آن‌را درک کنند.
  • مقرون به‌صرفه: هزینه توصیف آن کم است.

مهندسی نرم‌افزار سخت‌گیر
مهندسی نرم‌افزار سخت‌گیر راجع به طراحی و پیاده‌سازی و چرخه حیات نرم‌افزار عاری از نقص‌های منطقی یا کارکردی است؛ یعنی اجتناب از خطاها. لفط سخت‌گیر یعنی استدلال‌های عاری از خطا ریشه در علم کامپیوتر، منطق و ریاضی دارند تا مطالعه‌های تجربی و آماری.
مسئله، کیفیت نرم‌افزار است و اطمینان به اعتمادپذیری آن. هر چند که برای همه نرم‌افزارها کیفیت مهم است، وقتی اگر نرم‌افزار مورد بحث قرار باشد سیستم حیاتی همچون تجهیزات پزشکی و هسته‌ای را مدیریت کند، کیفیت بسیار ضروری می‌شود و همه تمرکز طراح و برنامه‌ساز را به خود معطوف می‌سازد.
نرم‌افزار اگر با روش‌های سنتی تولید شود، قطعاً بی‌خطا نیست. شرکت‌های سازنده نرم‌افزارها را با خطاهای شناخته شده و شناخته نشده عرضه می‌کنند. همچنین سیستم‌های خودکار گزارش اشکال نیز داخل نرم‌افزار تعبیه می‌کنند که در موقع بروز خطا اطلاعاتی به شرکت سازنده ارسال کند. شرکت نرم‌افزاری با این اطلاعات بهتر می‌تواند خرابی را تعمیر کند. آمارهای بسیاری راجع به حوادث و پیامدهای ناشی از نرم‌افزارهای معیوب موجود است. این آمار شاهدی از دو حقیقت مهم هستند:

  • هزینه نگهداری نرم‌افزار دو سوم کل هزینه نرم‌افزار است.
  • اگر وجود خطایی در توصیف و مشخصات نرم‌افزار بعد از عرضه معلوم شود، 20 برابر هزینه بیشتری دارد تا این خطا قبل از عرضۀ نرم‌افزار آشکار گردد.

پس درستی نرم‌افزار هزینه‌های مالی سنگین و هزینه‌های جانی غیرقابل جبران دارد. متأسفانه گواهی درستی نرم‌افزار به‌صورت مطلق، به‌شدت دشوار است. پس سعی می‌کنیم درجه اطمینان‌پذیری و اعتماد خود را به محصول نرم‌افزاری، با هر شیوه معقول و ممکن بالا ببریم.
مشهورترین روش تضمین درستی نرم‌افزار آزمون است. آزمون بسیار ساده است ولی آزمون جامع حداقل فعلاً غیرعملی است. با این حال، مهندسی آزمون، نظام بالغی است که تخصص در آن بسیار در صنعت جا افتاده است و رواج دارد.
غیر از آزمون، از روش‌های صوری هم می‌توان برای تضمین و بررسی اعتمادپذیری نرم‌افزار استفاده کرد. به‌خاطر پیشرفت چشمگیر ابزارها و زیرساخت‌های استفاده از روش‌های صوری، در سال‌های اخیر، استفاده از آن‌ها در صنعت رشد داشته است و رو به افزایش هم هست.
روش‌های صوری از مدل‌سازی ریاضی و حساب و منطق در توصیف مشخصات، طراحی، پیاده‌سازی و تحلیل سیستم‌های نرم‌افزار استفاده می‌کنند. در قلب روش‌های صوری مجموعه‌ای از ابزارهای ریاضی و نشانه‌گذاری‌ها و ساختاری صوری است که برای مدل‌سازی و استدلال در مورد سیستم‌های نرم‌افزاری (و سخت‌افزاری) استفاده می‌شوند. با روش‌های صوری امکان استدلال در مورد فضای کامل داده‌ها و پیکربندی سیستم فراهم می‌شود.
وقتی کل چرخه حیات نرم‌افزار از روش‌های صوری استفاده کند، یک روشگان (متدولوژی) سخت‌گیر برای توسعه نرم‌افزار شکل گرفته است. در حال حاضر وقتی قرار باشد برای سیستم‌های حیاتی که نیازمندی‌های خاصی دارند، نرم‌افزار بسازیم، از مهندسی نرم¬افزار سخت‌گیر استفاده می‌شود. سیستم‌های پزشکی، نظامی، فضاپیماها، نیروگاه‌ها، هواپیما، سیستم‌های کنترل صنعتی از نمونه¬های سیستم‌های حیاتی هستند.
مهندسی نرم‌افزار سخت‌گیر از روش‌های صوری برای توصیف نیازمندی‌های نرم‌افزار استفاده می‌کند و سپس طراحی و برنامه‌سازی را نیز بر اساس همین روش‌های صوری انجام می‌دهد. روش‌های صوری هم برای توصیف نیازمندی‌های کارکردی قابل استفاده‌اند و هم از آن‌ها می‌توان برای نیازمندی‌های غیرکارکردی مثل ایمنی حافظه، دسترسی‌های غیرمجاز، احراز اصالت و مجوزهای دسترسی استفاده نمود.
وقتی سراغ مهندسان صنعتی می‌رویم، این‌که روش‌های صوری اطمینان‌پذیری بیشتری فراهم می‌آورند، دلیل موجهی برای استفاده از آن‌ها نیست. دو عامل مهم باعث می‌شود در صنعت از روش‌های صوری استفاده شود:

  • واقعاً به آن نیاز داشته باشد؛
  • واقعاً از آن سود ببرد.

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

  • بلوغ و پایداری مفاهیم و ابزارهای زیربنایی
  • پشتیبانی ابزاری مناسب در کاربرد صنعتی
  • امکان کسب تخصص لازم و مهارت کافی برای استفاده درست
  • امکان یکپارچه‌سازی فنون و دانش مهندسی نرم‌افزار موجود با روش‌های صوری
  • درک و پذیرش تأثیر و هزینه‌های اولیه روش‌های صوری در شرکت

مطالبی که معمولاً برای استفاده از روش‌های صوری در مهندسی نرم‌افزار سخت‌گیر لازم هستند عبارتند از: منطق گزاره‌ها ، منطق مرتبه اول، منطق هور ، درستی‌آزمایی ، خصوصیات ایمنی و قراردادها .

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

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


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


مراجع

  • [1] Woodcock, J., & Davies, J. (1996). Using Z: specification, refinement, and proof (Vol. 39). Englewood Cliffs: Prentice Hall.
  • [2] Almeida, J. B., Frade, M. J., Pinto, J. S., & de Sousa, S. M. (2011). Rigorous software development: an introduction to program verification. Springer Science & Business Media.
  • [3] Kourie, D. G., & Watson, B. W. (2012). The Correctness-by-Construction Approach to Programming. Springer Science & Business Media.