ترجمه: زردشت هدایی
ماهنامه شبکه – شماره 68
اشاره :
کامپیوترها روز به روز بیشتر در زندگی ما دخیل می‌شوند. امروزه خطوط هوایی، عملیات بانکی، ارتباطات تجاری، سیستم‌های تولید و فروش و بسیاری بخش‌های حیاتی دیگر جامعه به کامپیوترها متکی شده‌اند. در چنین شرایطی خطا در نرمافزار می‌تواند نتایج فاجعه‌باری به بار بیاورد. بیشتر مشکلات عمده یک نرمافزار ریشه در اولین قدم ساخت آن، یعنی طراحی، دارد. برای پیشگیری از چنین مشکلاتی ابزارهای تحلیلی قدرتمندی ارائه شده‌اند که مهندسان نرمافزار می‌توانند به کمک آن‌ها از قابل اطمینان بودنِ نرم‌افزارهایشان مطمئن شوند.
منبع: ساینتیفیک‌امریکن
ضعف طراحی
افتتاح فرودگاه دنور در یازده سال پیش نمونه‌ای درخشان از معماری و فناوری‌های پیشرفته بود. سیستم خودکار توزیع و کنترل‌بار، گل سر سبد High-Tech در این فرودگاه بود. این سیستم، قرار بود مطلقاً بدون دخالت نیروی انسانی، بسته‌ها و چمدان‌ها را در طول 26 مایل مسیر‌های انتقال، جابه‌جا و توزیع کند و بار‌ها را به‌سرعت، به‌راحتی و با اطمینان به هواپیماها یا به‌دست مسافران برساند. ولی مشکلات نرم‌افزاری دائماً این سیستم را از کار می‌انداخت و نهایتاً موجب تأخیر شانزده ماهه در افتتاح فرودگاه و صرف میلیون‌ها دلار هزینه اضافه شد. به‌رغم اصلاحات بی‌شمار، این سیستم هیچ‌گاه نتوانست با اطمینان عمل کند تا این‌که بالاخره در تابستان گذشته مدیران فرودگاه تصمیم گرفتند آن را به کلی کنار بگذارند و دوباره از سیستم سنتی توزیع بار استفاده کنند. شرکتBAE Automated Systems، طراح سیستم توزیع بار خودکار، منحل شد و United Airlines مشتری اصلی این سیستم به مرز ورشکستگی کشیده شد.
طراحی ضعیف نرمافزار هر روز خشم میلیون‌ها کاربر را برمی‌انگیزد و هزینه‌های بالایی به آن‌ها و به شرکت‌ها تحمیل می‌کند. مثال‌هایی چون فرودگاه دنور کم نیستند. سازمان درآمدهای داخلی ایالا‌ت متحده در سال 1997 پروژه‌ای چهارمیلیارددلاری برای مدرن کردن فرایندهای کاری خود اجرا کرد که با شکست روبه‌رو شد.
به دنبال آن پروژه‌ای هشت میلیارد دلاری برای بهبود سیستم قبلی انجام شد که به همان اندازه پروژه اولی دردسرساز شد. اداره آگاهی فدرال (FBI) هم در سال 2005 سیستم 170 میلیون دلاری مدیریت الکترونیک پرونده‌ها را کنار گذاشت.
اداره هوانوردی فدرال هنوز هم با پروژه بی‌فرجام و پرهزینه نوسازی سیستم‌های قدیمی کنترل ترافیک هوایی دست‌وپنجه نرم می‌کند.
علت چنین شکست‌های عظیمی این است که اشتباهات طراحی خیلی دیر آشکار می‌شوند. فقط وقتی که برنامه‌نویسان نوشتن کد برنامه را شروع می‌کنند، متوجه ناکارآمدی و مشکلات طراحی خود می‌شوند. گاهی مشکلات نرم‌افزاری به خاطر یک ناسازگاری یا فراموشکاری فاحش رخ می‌دهند، ولی در اکثر موارد ضعف و ابهام در طراحی کلی و ابتدایی نرمافزار باعث بروز مشکل می‌شود. البته همانطور که کد برنامه با افزودن تدریجی اصلاحات بزرگ‌تر می‌شود، یک ساختار طراحی مبسوط و پر جزئیات هم برای آن به وجود می‌آید.
البته چنین طرحی پر از موارد خاص، نقاط ضعف، و فاقد اصول یکدست و منسجم است؛ درست مثل ساختمان سازی، در نرمافزار هم اگر پی و بنیاد یک نرمافزار ضعیف و ناپایدار باشد، ساختاری نیز که روی آن بنا می‌شود، ناپایدار خواهد بود.
توسعه‌دهندگان و مدیرانی که نرم‌افزارهایشان با شکست‌های عمومی و بزرگ روبه‌رو شده است، می‌توانند در دفاع از خود بگویند، ما از شیوه‌های استاندارد و جا افتاده این صنعت استفاده کردیم؛ و متأسفانه حق هم دارند! توسعه‌دهندگان به ندرت طرح‌های خود را با دقت و به تفصیل مشخص می‌کنند و آن‌ها را برای داشتن ویژگی‌های مطلوب، تحلیل و بررسی می‌نمایند، ولی در دنیای امروز که کامپیوترها هواپیماها را هدایت می‌کنند، ماشین‌ها و قطارها را می‌رانند، بخش عمده‌ای از امور مالی را به عهده دارند، و دستگاه‌های تولید و تجارت را می‌گردانند، نیاز مبرمی به افزایش قابلیت اطمینان نرم‌افزارها احساس می‌شود.
در این میان، نسل جدیدی از ابزارهای طراحی نرمافزار در حال ظهور هستند. موتور تحلیل در این ابزارها از نظر روش کار شبیه ابزارهایی است که مهندسان برای بررسی طراحی سخت‌افزار کامپیوتر به کار می‌برند. توسعه‌دهنده با استفاده از یک زبان کدگذاری سطح بالا نرمافزار را مدل‌سازی می‌کند و بعد با استفاده از یک ابزار دیگر میلیاردها حالت مختلف اجرای سیستم را بررسی می‌نماید و به دنبال حالت‌‌های غیر عادی می‌گردد که می‌تواند موجب رفتار نامطلوب در سیستم شود.
این فرایند کوچک‌ترین خطاهای طراحی را حتی قبل از این‌که نرمافزار کدنویسی شود، مشخص می‌کند و از آن مهم‌تر، حاصل آن طراحی‌ای دقیق، مستحکم و جامع است که تمام وضعیت‌های متصور برای آن بررسی شده است. یک نمونه از این ابزارها، Alloy است که من (دانیل جکسون، نویسنده مقاله) به همراه تیم تحقیقاتیم ساخته‌ایم/ Alloy (که به صورت رایگان روی وب در دسترس است) توانایی‌های خود را در انواع کاربردها نظیر نرم‌افزارهای هوا – فضا، سیستم‌های تلفن، سیستم‌های رمزنگاری، و حتی طراحی ماشین‌هایی که در درمان سرطان به کار گرفته می‌شوند، نشان داده است.
تقریباً تمام مشکلات مهم یک نرمافزار را می‌توان در خطاهای مفهومی‌ای که قبل از شروع برنامه‌نویسی آن رخ داده است، ریشه‌یابی کرد. Alloy و سایر ابزارهای آزمون طراحی مشابه آن، بر حاصل تحقیقاتی که در یک ربع قرن برای اثبات درست بودن برنامه‌ها به کمک ریاضیات صورت گرفته‌اند، مبتنی هستند.
اما این ابزارها به جای این‌که این قضیه را دستی حل کنند، از ابزارهای منطقی خودکار بهره می‌گیرند که طرح نرمافزار را به عنوان یک معمای عظیم در نظر می‌گیرد که باید حل شود. این ابزارهای تحلیلگر، روی طرح یک نرمافزار کار می‌کنند و نه کد آن. بنابراین، تضمین نمی‌کنند که یک نرمافزار با مشکل مواجه نشود. اما این‌ها نخستین ابزارهای عملی‌ای هستند که مهندسان نرمافزار می‌توانند به کمکشان مطمئن شوند که طراحی یک نرمافزار مستحکم و فاقد خطاهای مفهومی است و بنابراین پایه‌ای قوی است که می‌توان روی آن یک سیستم نرم‌افزاری مطمئن و قابل اطمینان را بنا نهاد.
ارزیابی طراحی‌ها
نرمافزار بد، مشکل نوظهوری نیست. هشدارها درباره بحران نرم‌افزاری سابقه‌ای از دهه 1960 دارد و با گسترش استفاده از کامپیوتر در جامعه، این هشدارها فقط شدیدتر شده‌اند.
امروزه معمولاً تمام نرم‌افزارها از طریق تست کردن، دیباگ و بهینه می‌شوند. مهندسان نرمافزار برنامه را با مجموعه وسیعی از مقادیر ورودی تست می‌کنند تا مطمئن شوند که به خوبی عمل می‌کند. این شیوه عده زیادی از خطاهای کوچک را آشکار می‌کند، ولی نمی‌تواند خطاهای اساسی موجود در طراحی اولیه نرمافزار را مشخص کند. به زبان دیگر، خانه از پای بست ویران است، خواجه در بند نقش ایوان است.
نکته بدتر این‌که، خود اصلاح باگ‌ها در مرحله تست نرمافزار، اغلب موجب بروز مشکلات طراحی می‌شوند. همانطور که برنامه‌نویسان کدها را دیباگ می‌کنند و قابلیت‌های جدیدی به آن‌ها می‌افزایند، بدون استثنا به پیچیدگی‌های برنامه افزوده می‌شود و امکان بروز مشکلات و ناکارآمدی در عملکرد برنامه بیشتر می‌شود.
این وضعیت یاد‌آور نظریه غلط بطلمیوسی در باب حرکت سیارات است که در یونان باستان ارائه شد. طبق نظر بطلمیوس، هر یک از سیارات بر مدار دایره‌ای حرکت می‌کردند که مرکز آن بر محیط دایره دیگری قرار داشت. در قرون وسطی مشاهدات نشان داد که برخی پیش‌بینی‌های این نظریه اشتباه بوده‌اند و دانشمندان آن زمان سعی کردند با افزودن دوایر دیگری به دوایر موجود، نظریه را اصلاح کنند.
اما این اصلاحات جزئی در طی قرون نتوانست مشکلات این نظریه را حل کند؛ چراکه مفاهیم بنیادی و اولیه‌ای که این نظریه بر آن‌ها استوار بود، اشتباهات فاحشی داشتند.
به همین ترتیب، نرم‌افزاری که از اول بد طراحی شده باشد، به‌رغم زمان و پول زیادی که صرف بهبود آن می‌شود، به تدریج پیچیده‌تر می‌شود و قابلیت اطمینان آن کمتر می‌گردد. امروزه روشن شده است که مشکلات جدی یک سیستم نرم‌افزاری، از خطاهای برنامه‌نویسی ناشی نمی‌شوند. تقریباً تمام مشکلات عمده یک نرمافزار را می‌توان در خطاهای مفهومی‌ای که قبل از شروع برنامه‌نویسی آن رخ داده است، ریشه‌یابی کرد. صرف کمی زمان و هزینه برای تحلیل و مدل کردن در مراحل اولیه تعیین نیاز‌ها، ویژگی‌ها و طراحی یک نرمافزار، در مقابل هزینه‌هایی که باید برای بررسی تمام کدها بپردازیم، بسیار ناچیز است، ولی سود حاصل از آن بسیار زیاد است. تمرکز روی طراحی در ابتدای کار، جلوی بسیار از دردسرهای آینده را می‌گیرد.
ظهور ابزارهای طراحی نرمافزار به این دلیل با کندی مواجه بوده است که نرمافزار تابع قوانین فیزیکی نیست. برنامه‌های کامپیوتری اساساً همانند اشیایی ریاضی هستند که مقادیر آن‌ها با بیت‌ها ساخته می‌شوند. به همین دلیل، برنامه‌های نرم‌افزاری اشیایی گسسته (مانند ذرات) هستند، نه پیوسته. یک مهندس مکانیک می‌تواند یک قطعه را تحت تنش یک نیروی بزرگ تست کند و نتیجه بگیرد که اگر این تنش را تحمل کرد، می‌تواند نیروهای کوچک‌تر را هم تحمل کند. وقتی یک شی تابع قوانین و اصولِ (اکثرا پیوسته) فیزیکی است، تغییر کوچکی در یک کمیت معمولاً تغییر کوچکی در کمیت دیگری را برای آن به دنبال خواهد داشت، اما متأسفانه چنین قوانین کلی و سر راستی در جهان نرمافزار وجود ندارد و کسی نمی‌تواند از آزمون‌ها و مشاهدات موجود، نتیجه‌گیری مستقیم و قطعی داشته باشد. اگر بخشی از نرمافزار به درستی کار می‌کند، هیچ ربطی به نحوه کار بخش دیگری مشابه آن ندارد. دو بخش نرمافزار، اشیای گسسته و جدا از هم هستند.
در اولین روزهای ظهور علوم کامپیوتر، محققان امیدوار بودند برنامه‌نویسان هم بتوانند درست همانطور که ریاضیدانان درستی قضیه‌هایشان را اثبات می‌کنند، درستی کدهایی را که نوشته‌اند اثبات کنند. در آن زمان هیچ راهی برای خودکار‌سازی بررسی مراحل بی‌شمار این‌کار وجود نداشت و متخصصان مجبور بودند بخش اعظم کار را به صورت دستی انجام دهند؛ جز برای برنامه‌هایی که از لحاظ پیچیدگی نسبتاً معمولی و از لحاظ اهمیت بسیار حیاتی بودند: مثلاً در الگوریتمی برای کنترل خطوط راه‌آهن، چنین روش‌های دشوار و دقیقی غیرعملی می‌نمود.
در سال‌های اخیر محققان روش کاملاً متفاوتی ابداع کرده‌اند که از توانایی پردازنده‌های قوی امروزی برای آزمون تمام سناریوهای ممکن بهره می‌گیرد.
این روش که به آن چک‌کردن مدل (Model Checking) می‌گویند، در حال حاضر به طور گسترده برای بررسی طراحی مدارهای مجتمع به کار گرفته می‌شود. ایده این روش این است که هر سلسله از وضعیت‌های ممکنی را که یک سیستم در عمل ممکن است با آن روبه‌رو شود بررسی کنیم و مطمئن شویم که هیچ یک از آن‌ها منجر به شکست سیستم نخواهد شد. منظور از وضعیت (State)، شرایط سیستم در هر زمان مشخص است. برای یک میکروچیپ تعداد وضعیت‌هایی که باید بررسی شود، اغلب بسیار بزرگ است؛ چیزی حدود 10 به توان 100 یا بیشتر! بررسی وضعیت‌ها برای یک نرمافزار بسیار دشوارتر است. اما تکنیک‌های هوشمندانه‌ای برکدگذاری وجود دارد که به کمک آن‌ها می‌توان مجموعه‌های بزرگی از وضعیت‌های یک نرمافزار را به طور خیلی فشرده بیان کرد. با استفاده از این تکنیک‌ها می‌توان این مجموعه‌های بزرگ را به طور همزمان بررسی کرد و به این ترتیب تمام وضعیت‌های ممکن یک نرمافزار را آزمایش کرد.
متأسفانه مدل فوق به تنهایی نمی‌تواند از عهده بررسی وضعیت‌هایی با ساختارهای پیچیده برآید. درحالی که طراحی‌های نرمافزار اکثراً چنین ویژگی‌ای دارند. من و همکارانم شیوه‌ای ابداع کرده‌ایم که از همان ایده بهره می‌گیرد، ولی سازوکار متفاوتی را به کار می‌بندد. شیوه ما هم مثل مدل checking تمام سناریوهای ممکن برای یک سیستم را در نظر می‌گیرد. البته واقعیت این است که برای این‌که مسئله در حدود متناهی قرار بگیرد، مجبوریم مرزهایی برای آن در نظر بگیریم؛ چراکه نرمافزار همانند سخت‌افزار تابع محدودیت‌های فیزیکی نیست. با این حال تکنیک ما، برخلاف مدل چکینگ، سناریوهای مختلف را یکی یکی تا انتها بررسی نمی‌کند، بلکه سناریوی بد (سناریویی که منجر به شکست خواهد شد) را جست وجو می‌کند. شیوه کار به این صورت است که برنامه به صورت خودکار و بدون هیچ ترتیب مشخصی وضعیت‌های مختلف را یکی یکی کنار هم می‌گذارد تا نهایتاً به سناریویی برسد که منجر به شکست سیستم خواهد شد.
این فرایند را تاحدی می‌توان با یک بازوی روباتیک مقایسه کرد که قطعات مختلف یک پازل تصویری را کنار هم می‌چیند تا نهایتاً تصویر کامل به دست آید. اگر تصویر به دست آمده یک سناریوی بد را نشان دهد، Alloy به هدفش رسیده است. به این ترتیب Alloy تحلیل طراحی را مانند معمایی در نظر می‌گیرد که باید حل شود. بعضی از نرم‌افزارهای دیگر مدل چکینگ که اخیرا ساخته شده‌اند هم از چنین شیوه‌ای استفاده می‌کنند.
راه‌حل، یک پازل است!
برای این‌که بفهمید Alloy چطور معمای طراحی نرمافزار را حل می‌کند، بد نیست به یک معمای قدیمی اشاره کنیم: یک کشاورز به بازار می‌رود و یک روباه، یک غاز، و یک کیسه ذرت می‌خرد. در راه برگشت به خانه، باید با قایق از یک رودخانه رد شود، ولی قایق در هر بار فقط می‌تواند او و فقط یکی از خریدهایش را ببرد. مشکل اینجاست که اگر او نباشد، روباه غاز را می‌خورد و غاز ذرت را. حالا کشاورز چطور خریدهایش را سالم به آن طرف رودخانه ببرد؟
در این نوع معماها هدف یافتن سناریویی است که با مجموعه‌ای از قیدها سازگار باشد. روش ما انسان‌ها برای حل اینگونه معماها این است که مجموعه‌ای از مراحل را در ذهن خود تصور می‌کنیم: کشاورز اول غاز را می‌برد. بعد برمی‌گردد و روباه را می‌برد و این‌بار در برگشت غاز را با خود برمی‌گرداند. بعد غاز را می‌گذارد و ذرت را می‌برد و نهایتاً برمی‌گردد و غاز را می‌برد. با بررسی این‌که آیا هر یک از مراحل با قیدها مطابقت دارد، ما مطمئن می‌شویم که معما درست حل شده است.
در یک طراحی موفق نرمافزار هم، چنین قیدهایی وجود دارد، اگرچه بسیار پیچیده‌تر هستند. هدف یک ابزار بررسی طراحی این است که مثال‌های نقض برای طراحی پیدا کند: یعنی راه حل‌هایی برای معما که با همه قید‌های خوب مطابقت دارند (بنابراین وقتی برنامه اجرا می‌شود، می‌توانند اتفاق بیفتند) و علاوه بر آن حداقل با یک قید بد هم سازگارند (بنابراین می‌توانند منجر به نتیجه‌ای نامطلوب شوند).
هرگاه یک مثال نقض به این ترتیب پیدا شود، نشان‌دهنده خطا در طراحی است. بنابراین، اگرچه ابزارِ معماحل کن از پیدا کردن راه حل معمای کشاورز خوشحال می‌شود، جواب معمای طراحی نرمافزار خبر شادی‌بخشی نیست. چون نشان می‌دهد که یک سناریوی نامطلوب وجود دارد و طراحی نرمافزار ایراد دارد.
در عمل، مثال نقض ممکن است خودش مستقیماً به یک مشکل منجر نشود، بلکه ممکن است نشان دهد که طراح از اول نتایج غیرقابل قبول را خوب مشخص نکرده است و ویژگی‌های آن‌ها را به درستی تعیین ننموده است. به هرحال، در هردو صورت چیزی باید اصلاح شود؛ یا خود طراحی، یا پیش‌فرض‌ها و انتظارات طراح.
هدف این است که هریک از وضعیت‌هایی را که نرمافزار ممکن است داشته باشد، شبیه‌سازی کنیم تا مطمئن شویم که هیچ یک منجر به شکست نخواهد شد.
دشواری اصلی در جست‌وجو برای مثال‌های نقض این است که تعداد سناریوهای بالقوه حتی در طراحی نرم‌افزاری با پیچیدگی متوسط، غالباً بسیار زیاد است، ولی فقط کسر بسیار کوچکی از این سناریوها مثال نقض هستند. فرض کنید می‌خواهید برنامه‌ریزی کنید که در یک مهمانی عروسی چه کسی کنار چه کسی بنشیند. اگر همه حاضران با هم دوست باشند، راه حل چندان دشوار نیست.
اما اگر مثلاً چند نفر از آن‌ها قبلاً با هم دوست بوده‌اند و حالا با هم قهرند، نباید آن ها را کنار هم نشاند و این مسئله را سخت‌تر می‌کند. حالا تصور کنید که مهمانی عروسی مال رومئو و ژولیت است.(1) اگر فقط بیست صندلی داشته باشیم و هریک از ده نفر مهمان بتواند آزادانه روی هر صندلی که خواست بنشیند، تعداد ترکیب‌های ممکن برابر 10 به توان 20 حالت خواهد بود. یک کامپیوتر حتی اگر بتواند در هر ثانیه یک میلیارد سناریو را بررسی کند، باز به سه‌هزار سال وقت برای بررسی همه حالت‌ها نیاز دارد.
در دهه 1980، محققان ریاضیات مسائلی از این دست را تحت عنوان کلاس خاصی از مسائل طبقه‌بندی کردند که در بدترین حالت برای حل آن‌ها باید تمام حالت‌‌های ممکن را تک تک بررسی کرد، ولی در دهه گذشته با ابداع استراتژی‌ها و الگوریتم‌های جدید جست‌وجو و افزایش روزافزون قدرت محاسباتی، محققان ابزارهایی به اسم SAT solver (حل‌کننده SAT) ساخته‌اند که می‌توانند چنین مسئله‌هایی را نسبتاً به آسانی حل کنند.(2) در حال حاضر انواع مختلفی از SAT solverها به صورت رایگان در دسترس هستند که می‌توانند مسائلی با میلیون‌ها قید را حل کنند.
اهمیت انتزاعی عمل کردن
Alloy (آلیاژ) همانطور که از نامش پیداست، از ترکیب دو عنصر برای کمک به قوی‌تر کردن طراحی نرمافزار بهره می‌گیرد. یکی از آن‌ها زبان جدیدی است که به کمک آن می‌توان ساختار و رفتار نرمافزار را توضیح داد. دیگری تحلیلگر خودکاری است که با استفاده از یک SAT solver تمام سناریوهای ممکن را بررسی می‌کند.
اولین مرحله در استفاده از Alloy، ساختن یک مدل از طرح نرمافزار است.
منظور از مدل یک طرح ابتدایی یا فلوچارت‌هایی نیست که معمولاً مهندسان نرمافزار به کار می‌گیرند، بلکه منظور یک مدل دقیق است که به تفصیل، تمام اجزا نرمافزار را شرح می‌دهد و رفتارهای آن‌ها را اعم از مطلوب و نامطلوب مشخص می‌کند. طراح نرمافزار ابتدا تعریفی از تمام اشیای مختلف موجود در طرح می‌نویسد و بعد این اشیا را در مجموعه‌های ریاضی دسته‌بندی می‌کند. مجموعه، یعنی دسته‌ای از اشیا که ساختار و رفتار مشابه دارند (مثلاً همه از خانواده کاپولت هستند) و با روابط ریاضی به هم مرتبطند (مثلاً رابطه بین مهمان‌هایی که می‌توانند کنار‌هم بنشینند.)
پس از آن، واقعیت‌ها (fact) بیان می‌شوند که مجموعه‌ها و رابطه‌ها را محدود می‌کنند. در طراحی نرمافزار واقعیت‌ها شامل مکانیسم‌های سیستم نرم‌افزاری و فرض‌هایی درباره دیگر اجزا است (مثلاً گزاره‌هایی درباره رفتار احتمالی کاربران سیستم). بعضی از این واقعیت‌ها فرض‌های واضحی هستند (مثلاً این‌که هیچ کس نمی‌تواند هم کاپولت و هم مونتاگو باشد و این‌که هر مهمان دقیقاً در کنار دو مهمان دیگر خواهد نشست) و بعضی از آن‌ها از خود طراحی ناشی می‌شوند؛ برای نمونه در مثال ما، این قانون که هر میز، جز میز بالا‌ی مجلس، باید فقط به اعضای یک خانواده اختصاص داشته باشد.
نهایتاً، حکم‌ها (assertion) قرار می‌گیرند که قیدهایی هستند که از واقعیت‌ها ناشی می‌شوند.به عنون نمونه در مثال ما، جز رومئو و ژولیت، هیچ کاپولتی نباید کنار یک مونتاگو بنشیند. حکم‌ها می‌گویند که سیستم هرگز نمی‌تواند دچار بعضی وضعیت‌های نامطلوب شود و سلسله‌های مشخصی از رویدادهای بد، هرگز نمی‌توانند اتفاق بیفتند.
بخش تحلیلگر Alloy برای یافتن مثال‌های نقض از یک SAT solver استفاده می‌کند. مثال‌های نقض سناریوهای احتمالی در یک سیستم نرم‌افزاری هستند که طراحی سیستم اجازه رخ دادن آن‌ها را می‌دهد، ولی نمی‌توانند آزمون درستی (sanity check) را پشت سر بگذارند. آزمون درستی با نوشتن حکم‌هایی که اگر طراحی مدل درست باشد، مقدار آن‌ها درست (True) می‌شود، انجام می‌شود. به زبان دیگر، این ابزار سعی می‌کند شرایطی را پدید آورد که با واقعیت‌ها مطابقت دارند، ولی حداقل یک حکم بیان شده را زیر پا می‌گذارند. مثلاً در مثال ما، ممکن است ترتیبی برای نشستن افراد پیدا کند که طی آن در میز بالا‌ی مجلس یک کاپولت (غیر از ژولیت) کنار یک مونتاگو (غیر از رومئو) بنشیند. برای این‌که جلوی رخ دادن چنین سناریویی را بگیریم، می‌توانیم در طرح نرم‌افزارمان یک واقعیت جدید اضافه کنیم: فقط رومئو و ژولیت پشت میز بالا‌ی مجلس می‌نشینند. حالا دیگر Alloy نمی‌تواند مثال نقضی پیدا کند.
به کمک Alloy مشکلات جدی موجود در بعضی از طرح‌های نرم‌افزاری موجود مشخص شده است. مشخص کردن مجموعه‌ها، رابطه‌ها، واقعیت‌ها، و حکم‌ها به اتفاق، یک انتزاع می‌سازد که یک طرح نرم‌افزاری را دقیقاً شرح می‌دهد. نوشتن تمام این‌ها با دقت و به تفصیل موجب آشکار شدن ایرادات طراحی می‌شود و مهندسان مجبور می‌شوند درباره این‌که چه انتزاعی (abstraction) مناسب‌تر است، بیشتر فکر کنند. اساس بسیاری از سیستم‌های نامطمئن و بیش از حد پیچیده به انتخاب انتزاعی غلط باز می‌گردد.
در مقابل، اگر دقت کنیم، می‌بینیم که سیستم‌هایی که در آن‌ها نرمافزار بر اساس یک انتزاعی ساده و قوی ساخته شده است، نه تنها قوی‌ترند، بلکه حتی استفاده از آن‌ها هم ساده‌تر است. مثلا ًe-Ticketing را در نظر بگیرید که چطور مسافرت‌های هوایی را راحت‌تر کرده است یا کد جهانی کالا (UPC) که چطور موجب سهولت فروش شده است، یا تلفن‌های معاف از مالیات با پیش‌شماره هشتصد که تله‌کنفرانس را ساده‌تر ساخته‌اند. در تمام این نوآوری‌ها شاهد تحولی در انتزاعی هستیم که نرمافزار بر اساس آن ساخته شده است.
قابلیت اطمینان نرم‌افزارها در آینده
در حال حاضر ابزارهایی مثل Alloy بیشتر در تحقیقات و سیستم‌های صنعتی فوق پیشرفته به کار گرفته می‌شوند. این فناوری برای بررسی معماری‌های جدید در سیستم‌های سوییچینگ تلفن، برای طراحی پردازنده‌های به کار رفته در صنعت هوانوردی و سیستم‌های ایمن در مقابل حمله هکرها، و برای وضع سیاست‌‌های کنترل دسترسی در شبکه‌های ارتباطاتی به کار گرفته شده است.
همچنین با استفاده از این فناوری برخی مکانیسم‌های نرم‌افزاری مهم و پر استفاده را نیز بررسی کردیم؛ برای مثال، پروتکل‌هایی که برای یافتن چاپگرها در شبکه به کار می‌روند یا ابزارهایی برای همزمان‌سازی فایل‌ها بین کامپیوترهای مختلف.
علاوه بر این، Alloy برخی مشکلات جدی در طراحی نرم‌افزارهای موجود را نیز آشکار کرده است. از جمله یک پروتکل مهم مدیریتی که می‌بایست بر اساس عضویت در گروه‌ها، قوانین دسترسی مخصوصی را اعمال می‌کرد، ولی ممکن بود به اعضای سابق یک گروه که باید دسترسی آن‌ها منع می‌شد نیز مجوز بدهد. قابل‌توجه است که بسیاری از برنامه‌نویسانی که از Alloy استفاده کردند، از تعداد خطاهای طراحی‌ای که این ابزار حتی در ساده‌ترین برنامه‌های آن‌ها پیدا کرد، شگفت زده شدند.
ابزارهایی مثل Alloy به احتمال زیاد در آینده به طور گسترده‌تری در صنعت به کار گرفته خواهند شد. با بهبود SAT solverهای به کار رفته در این ابزارها، آن‌ها می‌توانند سیستم‌های بزرگ‌تر را بهتر و سریع‌تر بررسی کنند. در عین حال نسل جدید طراحان نرمافزار که با این روش‌ها آشنایی دارند، از آن‌ها در کار خود استفاده خواهند کرد. در حال حاضر استفاده از مدلینگ رو به گسترش است؛ به‌ویژه از سوی مدیرانی که دوست دارند برای توصیف یک نرمافزار چیزی بیشتر از کد برنامه آن را ببینند.
به هر حال روزی خواهد رسید که نرمافزار چنان در تار و پود زندگی روزمره ما رسوخ کند که جامعه دیگر پذیرای نرمافزار بد نباشد. در نتیجه دولت‌ها از هم اکنون باید به فکر وضع استانداردها، مقررات و مجوزهایی باشند که استفاده از تکنیک‌های پیشرفته و ساخت نرم‌افزارهای با کیفیت را الزام‌آور سازند. بالاخره روزی تمام سیستم‌های نرم‌افزاری واقعاً قابل اعتماد، قابل پیش بینی و سهل‌الاستفاده خواهند بود و این ویژگی‌ها را از همان اولین قدم، یعنی مرحله طراحی خواهند داشت.
پی‌نوشت‌های مترجم:
1- رومئو و ژولیت از دو خانواده به اسم کاپولت‌ها و مونتاگوها بودند که با هم اختلا‌ف داشتند.
2- SAT از اصطلاح satisfiability (انجام‌پذیری) در منطق گزاره‌ای گرفته شده است.
