مقاله طراحی یک نرم‌افزار مطمئن

[Fahim 9,563]

وابستگی به کامپیوتر و سیستم‌های نرم‌افزاری تقریباً در تمام جنبه‌های زندگی روزمره به سرعت در حال افزایش است و این وابستگی به شکلی است که ما حتی در بسیاری موارد، از وجود و نقش کامپیوتر و نرم‌افزار در آن‌ها بی‌اطلاع هستیم. بسیاری از امور کنترلی در خودروهای امروزی از قبیل ترمز، کیسه هوا، کنترل موتور و سوخت‌رسانی بر پایه نرم‌افزارهای تعبیه‌شده(Embedded) در سيستم كامپيوتري خودرو کار می‌کنند. تلفن‌های همراه، سیستم‌های ارتباطی، دستگاه‌های پزشکی، سیستم‌های صوتی و تصویری و همچنین حمل و نقل و راه و ترابری، سیستم‌های تولیدی و کنترلی و بسیاری از تجهیزات الکترونیکی در کل برای افزایش کارایی، انعطاف‌پذیری بیشتر و کاهش هزینه، به میزان زیادی از نرم‌افزارها استفاده می‌کنند. در اين ميان برخي سيستم‌ها به نحوی با جان و مال انسان‌ها سر و‌کار دارند و بروز خطا و خرابی در آن‌ها موجب خسارت‌های جبران‌ناپذیری خواهد شد. طراحی این سیستم‌ها که از آن‌ها تحت عنوان سیستم‌های حساس و حیاتی (Safety-Critical) یاد می‌کنیم باید به گونه‌ای کاملاًً مطمئن انجام شود.

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

برای مشاهده این محتوا لطفاً ثبت نام کنید یا وارد شوید.

• ورود
• یا
• ثبت نام

شكل 1- هزينه‌هاي مطرح شدن، كشف و اصلاح عيوب در طول چرخه حيات نرم‌افزار

 

وجود اشکال در نرم‌افزارهای پیچیده‌ای همچون ویندوز، در نهایت به توقف سیستم و شروع دوباره دستگاه و در بدترین شرایط به از دست رفتن اطلاعات منجر می‌شود که در اغلب موارد اگر آن اطلاعات به معنای واقعی، حیاتی‌باشد قبلاً نسخه پشتیبان از آن تهیه شده است. صرف نظر از امکان انجام آزمايش کامل این نرم‌افزار، اهمیت این مسئله در نگاه کلی به قدری نیست که شرکت سازنده آن چندین سال با قدرتمندترین سخت‌افزارهای پردازشی، آن را بررسی کرده و در نهایت آن را به ناچار با قیمت چند میلیون دلار روانه بازار کند! اما وجود خطای نرم‌افزاری در یک موشک فضایی مانند Araine-5 می‌تواند موجب انفجار آن تنها در 36 ثانیه پس از پرتاب شود. نمونه‌هایی از این قبیل در تاریخ کم نبوده‌اند. به ‌عنوان مثال، وجود اشکال در بخش کنترل ماشین پرتودرمانی Therac-25 موجب تششع بیش از اندازه امواج رادیواکتیو و مرگ شش بیمار سرطانی شد. در نمونه‌ای ديگر كه خوشبختانه تلفات جاني در پي داشت، خطای نرم‌افزاری در سیستم تحویل بار مسافران موجب تأخیر نه ماهه افتتاح فرودگاه دنور (Denver) و ضرر روزانه 1/1 میلیون دلار شد که در نوع خود خسارت سنگینی به شمار می‌رود. یا به عنوان نمونه خطاي سخت‌افزاری در طراحی، می‌توان به وجود خطا در بخش تقسیم ممیز شناور در پردازنده‌های پنتیوم2 اینتل اشاره کرد که در اوایل دهه 90 موجب جمع‌آوری پردازنده‌ها از بازار و ضرر 475 میلیون دلاری و از سوی دیگر ضربه خوردن به شهرت و اعتبار این شرکت به عنوان یکی از بزرگ‌ترین تولیدکنندگان تراشه در دنیا شد.

 

مرور دقیق (Peer Review)

مرور دقیق و آزمايش نرم‌افزار در عمل، عمده‌ترین روش‌هاي بررسی نرم‌افزارها به‌شمار می‌روند. مرور دقیق به طور معمول توسط یک تیم از مهندسان نرم‌افزار که عضو تیم توسعه سیستم تحت بازبینی نیستند، انجام می‌شود. کد کامپایل نشده و هنوز اجرا نشده است، اما به صورت ایستا و به‌طور کامل تحلیل و بررسی می‌شود. مطالعات تجربی نشان می‌دهد، مرور دقیق، یک روش مؤثر است که طی آن 31 تا 93 درصد و به‌طور میانگین 60 درصد عیوب سیستم کشف می‌شود. با این‌که این روش اغلب به صورت موردی و کلی انجام می‌شود، انواع اختصاصی‌تر از رویه‌های مرور دقیق، مانند زمانی که به دنبال اهداف خاصی از کشف خطا هستیم می‌تواند مؤثرتر واقع شود. می‌توان گفت، حدود هشتاد درصد تمام پروژه‌های نرم‌افزاری به شکلی از این روش استفاده مي‌كنند. تجربه نشان داده،‌ به دلیل ایستا بودن روش مرور دقیق، کشف خطاهای ظریف و کوچک از قبیل خطاهای مربوط به همزمانی اجرای دستورات و نقص‌های الگوریتم، با استفاده از این روش مشکل است.

"مرور دقیق (Peer Review)، یک روش مؤثر است که طی آن 31 تا 93 درصد و به‌طور میانگین 60 درصد عیوب سیستم کشف می‌شود."

 

 

آزمايش نرم‌افزار

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

 

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

برای مشاهده این محتوا لطفاً ثبت نام کنید یا وارد شوید.

• ورود
• یا
• ثبت نام

شكل 2 - شماي كنترل سيستم از طريق روش «بررسي مدل»

 

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

"مشکل دیگر در آزمايش نرم‌افزار، تشخیص زمان پایان دادن به این فرآیند است. در عمل، مشکل و گاهی غیرممکن است که مقدار آزمايش برای رسیدن به میزان مشخصی از چگالی عیوب را مشخص کنیم."

 

 

 

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

"مشکل دیگر در آزمايش نرم‌افزار، تشخیص زمان پایان دادن به این فرآیند است. در عمل، مشکل و گاهی غیرممکن است که مقدار آزمايش برای رسیدن به میزان مشخصی از چگالی عیوب را مشخص کنیم."

مطالعات نشان می‌دهد مرور دقیق و آزمايش، «دسته‌های متفاوتی» از خطاها را در «مراحل متفاوتی» از چرخه توسعه نرم‌افزار ،کشف می‌کنند و به همین دلیل، این دو روش نمی‌توانند جایگزینی برای یکدیگر به شمار آیند و به طور معمول در کنار هم به‌کار گرفته می‌شوند. در طراحی نرم‌افزارها گفته می‌شود، بهتر است هرچه زودتر خطاها را پیدا کنید. زيرا هزینه‌های جبران یک نقص نرم‌افزاری در زمان نگه‌داری به‌طورکلی پانصد برابر بیشتر از برطرف كردن یک مسئله در مراحل اولیه طراحی است. بنابراین، بررسی سیستم باید در مراحل آغازین فرآیند طراحی انجام شود. شکل 1 نموداری از هزینه‌های مطرح شدن خطاها، کشف و اصلاح آن‌ها را در چرخه حیات نرم‌افزار نمایش می‌دهد. با توجه به این نمودار حدود پنجاه درصد تمام نقص‌ها طی مدت برنامه‌نویسی، یعنی زمانی که کد نرم‌افزار نوشته می‌شود، مطرح شده و بيشتر خطاها هنگام آزمايش یافت می‌شوند. درحالی‌که تنها پانزده درصد تمام خطاها در مرحله طراحی اولیه کشف می‌شوند.

[Fahim 9,563]

بررسی مدل

دربیش از دو دهه گذشته، یکی از جذاب‌ترین دیدگاه‌ها برای بررسی درستی سیستم‌های کنترلی مبتنی بر کامپیوتر، بررسی مدل یا «Model Checking» بوده است. بررسی مدل روشي مبتنی بر ریاضیات برای آزمایش ویژگی‌های رفتاری مورد انتظار یک سیستم بر پایه یک مدل مناسب است که این کار از طریق امتحان و نظارت خودکار و قاعده‌مند روی تمام حالت‌های مدل انجام می‌شود.

"بزرگ‌ترین مشکل روش آزمايش مدل همان‌طور که پیش‌تر اشاره شد، انفجار فضای حالات است. با پردازنده‌ها و حافظه‌های کنونی، پیشرفته‌ترین ابزارهای بررسی مدل تنها قادر به بررسی فضای حالتی با بزرگی 108 تا 109 حالت هستند."

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

 

روش بررسی مدل، به یک مدل از سیستم و یک ویژگی مورد انتظار از آن سیستم نیاز دارد تا طی یک سری قواعد مشخص بررسی کند که آیا مدل داده شده، آن ویژگی را برآورده می‌کند یا خیر؟ از جمله مواردی که در بسیاری از سیستم‌ها بررسی می‌شوند، عدم وجود بن‌بست (Deadlock) در ویژگی‌های ثابت و تغییرناپذیر و درخواست-پاسخ های سیستم است. بن‌بست به حالتی گفته می‌شود که با رسیدن به آن حالت، سیستم دیگر قادر به پیشروی و گذار به حالت دیگر نباشد. نقص برنامه زمانی یافت می‌شود که سیستم در بررسی این ویژگی به اشکال برخورد کند و یک سیستم زمانی بدون اشکال تلقی می‌شود که در بررسی تمام انتظارات سیستم با اشکالی برخورد نکند. بنابراین، بدون اشکال بودن سیستم همواره با انتظاراتی که از آن سیستم داریم در رابطه است، نه ویژگی‌های مطلق آن. در شکل 2 شِمايي از بررسی درستی یک سیستم نشان داده شده است.

 

به دلیل پیشرفت‌های مداوم الگوریتم‌ها و ساختمان‌های داده و در کنار آن پیشرفت خیره‌کننده فناوری‌های سخت‌افزاری، بررسی مدل که دو دهه قبل تنها برای مثال‌های ساده کار می‌کرد، امروزه برای بسیاری از طرح‌های واقعی و عملی كاربردي است. به‌طوری که می‌توان از آن به عنوان یک روش کامل، پرکاربرد و مهم در بررسی و برطرف كردن خطا در دو دهه گذشته یاد کرد.در بررسی مدل از روش‌های فرمال استفاده می‌شود که تقريباً در ده تا پانزده درصد پروژه‌های نرم‌افزاری به‌کار می‌روند. اگر بخواهیم روش‌های فرمال را به اختصار معرفي کنیم، می‌توانيم بگوييم روش‌هایی بر پایه ریاضیات کاربردی هستند که برای مدل‌سازی و تحلیل سیستم‌های ICT با هدف بررسی صحت کارکرد سیستم با تکیه بر قدرت ریاضیات به کار می‌روند. روش‌های فرمال پتانسیل فراوانی در بررسی و صحت‌سنجی نرم‌افزار در فرآیند طراحی برای توسعه‌دهندگان دارد و به همین دلیل استفاده از آن در طراحی نرم‌افزارهای حساس و حیاتی به شدت توصیه شده است. استانداردهای مبنتی بر روش‌های فرمال در سازمان فضایی ناسا، IEC (سرنام International Electrotechnical Commission)، ESA (سرنام European Space Agency) و FAA (سرنام Federal Aviation Authority) نیز مؤید همین صحبت است.طی دو دهه گذشته، تحقیقات در روش‌های فرمال به توسعه روش‌هاي گوناگون بررسی و صحت‌سنجی منجر شده که کشف زود هنگام عیوب نرم‌افزارها را تسهیل کرده است. این روش‌ها به همراه ابزارهای نرم‌افزاری قدرتمندی که می‌تواند بسیاری از مراحل بررسی را به‌صورت خودکار در آورد، همراه شده و به این ترتیب موجب ایجاد تحولی در طراحی و تولید نرم‌افزارهای مطمئن شده است. بررسی‌ها نشان داده، رویه‌های بررسی فرمال می‌توانست بسیاری از عیوب نرم‌افزاری و سخت‌افزاری را از جمله اشکال موشک فضایی Ariane-5، پردازنده‌های پنتیوم2، ماشین پرتودرمانیTherac-25 و... را کشف کند. ضمن این‌که ماجول‌های فضاپیمای

Deep Space-1 ناسا که در سال 1998 به فضا پرتاب شد، با استفاده از روش بررسی مدل و روش‌های فرمال آزمایش شد. از آنجا که بررسی مدل رفتار سیستم، به شکلی دقیق و غیرمبهم به زبان ریاضی توصیف شده است، با استفاده از ابزارهای یاد شده می‌توان علاوه‌بر تشخیص خطا، ابهامات رفتاری، ناسازگاری‌ها، ناکامل بودن روش‌ها و... را نیز در فاز طراحی کشف کرد که این موارد در حالت معمول مدت‌ها بعد از گذشت فاز طراحی آشکار می‌شوند.

برای مشاهده این محتوا لطفاً ثبت نام کنید یا وارد شوید.

• ورود
• یا
• ثبت نام

شكل 3- «بررسي مدل»

 

می‌دانیم در بررسی مدل، تمام حالت‌های ممکن سیستم امتحان می‌شود. همانند بازی شطرنج کامپیوتری که قبل از هر حرکت، تمام حرکت‌های ممکن بررسی می‌شود، یک بررسی کننده مدل نیز با رفتاری مشابه در تمامی راه‌های ممکن، به دنبال راهی می‌گردد تا مثال نقضی برای برآورده نشدن یک ویژگی یا انتظار سیستم پیدا کند و با نرسیدن به این موفقیت، برآورده شدن آن انتظار را نتیجه می‌دهد. بزرگ‌ترین مشکل این روش همان‌طور که پیش‌تر اشاره شد، انفجار فضای حالات است. با پردازنده‌ها و حافظه‌های کنونی، پیشرفته‌ترین ابزارهای بررسی مدل تنها قادر به بررسی فضای حالتی با بزرگی 108 تا 109 حالت هستند. با استفاده از الگوریتم‌های هوشمند و ساختمان داده‌های مناسب برای مسائل به‌خصوص فضای حالات بزرگ‌تری به اندازه 1020 تا حتی 10476 حالت نیز قابل بررسی است. حتی پتانسيل كشف کوچک‌ترین و ظریف‌ترین خطاهایی که در مرور دقیق، آزمايش‌ها و شبیه‌سازی‌ها کشف نشده باقی می‌مانند، در صورت داشتن زمان، منابع کافی و مواجه‌نشدن با پدیده انفجار فضای حالات، وجود خواهد داشت. شکل 3 دیدگاه کلی بررسی مدل را به صورت خلاصه بیان می‌کند.

"هرگز نمی‌توان صد‌درصد تضمین داد یک سیستم در ابعاد واقعی بدون اشکال است. اما همچنان می‌توان از بررسی مدل به عنوان یک روش مؤثر و کارا برای کشف خطاهای احتمالی در طراحی استفاده کرد."

 

برای این‌که بررسی مدل با دقت بالا امكان‌پذير شود، ویژگی‌های سیستم باید به روشی دقیق و غیر مبهم توصیف شود. از مهم‌ترین و کلی‌ترین ویژگی‌های یک سیستم می‌توان به موارد زير اشاره کرد:

Safety: یک چیز بد هرگز رخ ندهد.

Liveness: یک چیز خوب همواره رخ بدهد.

Functional Correctness: آیا سیستم کاری را که از آن انتظار می‌رود انجام می‌دهد؟

Reachability: آیا حالات دلخواه سیستم از حالت آغازین دسترس‌پذیر است؟ آیا ممکن است سیستم با رسیدن به یک حالت بن‌بست، متوقف شود؟

Fairness: آیا تحت شرایط به‌خصوصی یک اتفاق به‌طور مکرر رخ می‌دهد؟

Realtime: آیا سیستم به موقع عمل می‌کند؟

هرکدام از این ویژگی‌ها در سیستم‌های مختلف تفسیرهای گوناگونی خواهد داشت که با توجه به ساختار سیستم و مدل مربوطه، بررسی شده و برقراری آن تأیید می‌شود.

 

نقات قوت

از مهم‌ترین نقاط قوت تکنیک بررسی مدل می‌توان به موارد زیر اشاره کرد:

- با توجه به این‌که بررسی مدل یک دیدگاه کلی برای صحت‌سنجی ارائه می‌کند، برای گستره وسیعی از برنامه‌ها مانند سیستم‌های تعبیه شده، مهندسی نرم‌افزار و طراحی سخت‌افزار كاربردي است.

- این روش از بررسی جزئی نیز پشتیبانی می‌کند. به بیان دیگر، می‌توان ویژگی‌ها را تک تک بررسی کرد و نیازی به تعیین کامل نیازمندی‌ها نیست. بنابراین، می‌توان اولویت بررسی را ابتدا به موارد مهم‌تر و ضروری‌تر اختصاص داد.

- درصورت وجود اشکال و کشف نادرستی یک ویژگی، اطلاعات مفیدی برای تشخیص و برطرف كردن آن تولید شده و در اختیار قرار خواهد گرفت.

- اين پتانسيل وجود دارد که کل کار تنها با فشار یک دکمه انجام شود و به‌طور کلی استفاده از تکنیک بررسی مدل، به تعامل یا درجه بالایی از تجربه و تخصص نیازی ندارد.

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

- به راحتي مي توان اين تكنيك را در چرخه فعلی توسعه نرم‌افزارها قرار داد و منحنی یادگیری آن چندان شیب‌دار نیست و مطالعات تجربی نشان داده که این کار زمان توسعه را کاهش می‌دهد.

- پایه ریاضی دقیقی دارد و بر پایه تئوری الگوریتم‌های گراف، ساختمان داده‌ها و منطق است.

 

 

نقاط ضعف

هر روش در کنار مزایایی که دارد، در بر گيرنده برخي از نكته‌هاي منفي است. از جمله نقاط ضعف روش بررسی مدل می‌توان به موارد

زیر اشاره کرد:

- به دلیل نا‌متناهی بودن داده‌ها، این روش اصولاً برای برنامه‌های کنترلی كاربردي است و برای برنامه‌هایی برپایه داده مناسب نیست.

- برای موضوعات تصمیم‌پذیر قابل استفاده است و برای سیستم‌های با حالات نامتناهی یا استدلال درباره انواع داده‌ای انتزاعی که به منطق‌های تصمیم‌ناپذیر یا نیمه‌تصمیم‌پذیر نیاز دارند،كاربردي نیست.

- این روش تنها مدل سیستم را بررسی می‌کند و خود سیستم واقعی یا نمونه آزمایشی آن را بررسی

نمی‌کند. بنابراین، روش‌های دیگر بررسی مانند آزمايش برای پیدا کردن خطاهای تولید و ساخت (برای سخت‌افزار) و همچنین یافتن اشکالات کدنویسی (برای نرم‌افزار) به عنوان مکمل این روش ضروري است.

- در این روش تنها نیازمندی‌های حالت‌دار بررسی می‌شوند و درباره درستی سایر ویژگی‌های بررسی نشده نمی‌توان نظری داد.

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

- برای یافتن برخی انتزاعات مناسب به منظور به‌دست آمدن مدل‌های کوچک‌تر به برخی تخصص‌ها و مهارت‌ها نیاز است.

- به دلیل آن‌که بررسی کننده‌های مدل نیز مانند هر نرم‌افزار دیگری ممکن است نقص نرم‌افزاری داشته باشند، تضمینی وجود ندارد که نتیجه تولید شده کاملاً درست باشد.

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

 

 

منبع : ماهنامه شبکه