طراحي نرم‌افزارهاي قابل اطمينان

[B O L O T]

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

[B O L O T]

ضعف طراحي‌
افتتاح فرودگاه دنور در يازده سال پيش نمونه‌اي درخشان از معماري و فناوري‌هاي پيشرفته بود. سيستم خودكار توزيع و كنترل‌بار، گل سر سبد High-Tech در اين فرودگاه بود. اين سيستم، قرار بود مطلقاً بدون دخالت نيروي انساني، بسته‌ها و چمدان‌ها را در طول 26 مايل مسير‌هاي انتقال، جابه‌جا و توزيع كند و بار‌ها را به‌سرعت، به‌راحتي و با اطمينان به هواپيما‌ها يا به‌دست مسافران برساند. ولي مشكلات نرم‌افزاري دائماً اين سيستم را از كار مي‌انداخت و نهايتاً موجب تأخير شانزده ماهه در افتتاح فرودگاه و صرف ميليون‌ها دلار هزينه اضافه شد. به‌رغم اصلاحات بي‌شمار، اين سيستم هيچ‌گاه نتوانست با اطمينان عمل كند تا اين‌كه بالاخره در تابستان گذشته مديران فرودگاه تصميم گرفتند آن را به كلي كنار بگذارند و دوباره از سيستم سنتي توزيع بار استفاده كنند. شركتBAE Automated Systems، طراح سيستم توزيع بار خودكار، منحل شد و United Airlines مشتري اصلي اين سيستم به مرز ورشكستگي كشيده شد.

طراحي‌ ضعيف نرم‌افزار هر روز خشم ميليون‌ها كاربر را برمي‌انگيزد و هزينه‌هاي بالايي به آن‌ها و به شركت‌ها تحميل مي‌كند. مثال‌هايي چون فرودگاه دنور كم نيستند. سازمان درآمدهاي داخلي ايالا‌ت متحده در سال 1997 پروژه‌اي چهارميليارددلاري براي مدرن كردن فرايندهاي كاري خود اجرا كرد كه با شكست روبه‌رو شد.

به دنبال آن پروژه‌اي هشت ميليارد دلاري براي بهبود سيستم قبلي انجام شد كه به همان اندازه پروژه اولي دردسرساز شد. اداره آگاهي فدرال (FBI) هم در سال 2005 سيستم 170 ميليون دلاري مديريت الكترونيك پرونده‌ها را كنار گذاشت.

اداره هوانوردي فدرال هنوز هم با پروژه بي‌فرجام و پرهزينه نوسازي سيستم‌هاي قديمي كنترل ترافيك هوايي دست‌وپنجه نرم مي‌كند.

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

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

توسعه‌دهندگان و مديراني كه نرم‌افزارهايشان با شكست‌هاي عمومي و بزرگ روبه‌رو شده است، مي‌توانند در دفاع از خود بگويند، ما از شيوه‌هاي استاندارد و جا افتاده اين صنعت استفاده كرديم؛ و متأسفانه حق هم دارند! توسعه‌دهندگان به ندرت طرح‌هاي خود را با دقت و به تفصيل مشخص مي‌كنند و آن‌ها را براي داشتن ويژگي‌هاي مطلوب، تحليل و بررسي مي‌نمايند، ولي در دنياي امروز كه كامپيوترها هواپيماها را هدايت مي‌كنند، ماشين‌ها و قطارها را مي‌رانند، بخش عمده‌اي از امور مالي را به عهده دارند، و دستگاه‌هاي توليد و تجارت را مي‌گردانند، نياز مبرمي به افزايش قابليت اطمينان نرم‌افزارها احساس مي‌شود.

در اين ميان، نسل جديدي از ابزارهاي طراحي نرم‌افزار در حال ظهور هستند. موتور تحليل در اين ابزارها از نظر روش كار شبيه ابزارهايي است كه مهندسان براي بررسي طراحي سخت‌افزار كامپيوتر به كار مي‌برند. توسعه‌دهنده با استفاده از يك زبان كدگذاري سطح بالا نرم‌افزار را مدل‌سازي مي‌كند و بعد با استفاده از يك ابزار ديگر ميلياردها حالت مختلف اجراي سيستم را بررسي مي‌نمايد و به دنبال حالت‌‌هاي غير عادي مي‌گردد كه مي‌تواند موجب رفتار نامطلوب در سيستم شود.

اين فرايند كوچك‌ترين خطاهاي طراحي را حتي قبل از اين‌كه نرم‌افزار كدنويسي شود، مشخص مي‌كند و از آن مهم‌تر، حاصل آن طراحي‌اي دقيق، مستحكم و جامع است كه تمام وضعيت‌هاي متصور براي آن بررسي شده است. يك نمونه از اين ابزارها، Alloy است كه من (دانيل جكسون، نويسنده مقاله) به همراه تيم تحقيقاتيم ساخته‌ايم/ Alloy (كه به صورت رايگان روي وب در دسترس است) توانايي‌هاي خود را در انواع كاربردها نظير نرم‌افزارهاي هوا - فضا، سيستم‌هاي تلفن، سيستم‌هاي رمزنگاري، و حتي طراحي ماشين‌هايي كه در درمان سرطان به كار گرفته مي‌شوند، نشان داده است.

تقريباً تمام مشكلات مهم يك نرم‌افزار را مي‌توان در خطاهاي مفهومي‌اي كه قبل از شروع برنامه‌نويسي آن رخ داده است، ريشه‌يابي كرد. ‌Alloy و ساير ابزارهاي آزمون طراحي مشابه آن، بر حاصل تحقيقاتي كه در يك ربع قرن براي اثبات درست بودن برنامه‌ها به كمك رياضيات صورت گرفته‌اند، مبتني هستند.

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

[B O L O T]

ارزيابي طراحي‌ها
نرم‌افزار بد، مشكل نوظهوري نيست. هشدارها درباره بحران نرم‌افزاري سابقه‌اي از دهه 1960 دارد و با گسترش استفاده از كامپيوتر در جامعه، اين هشدارها فقط شديدتر شده‌اند.

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

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

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

اما اين اصلاحات جزئي در طي قرون نتوانست مشكلات اين نظريه را حل كند؛ چراكه مفاهيم بنيادي و اوليه‌اي كه اين نظريه بر آن‌ها استوار بود، اشتباهات فاحشي داشتند.


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

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

در اولين روزهاي ظهور علوم كامپيوتر، محققان اميدوار بودند برنامه‌نويسان هم بتوانند درست همان‌طور كه رياضيدانان درستيِ قضيه‌هايشان را اثبات مي‌كنند، درستي كدهايي را كه نوشته‌اند اثبات كنند. در آن زمان هيچ راهي براي خودكار‌سازي بررسي مراحل بي‌شمار اين‌كار وجود نداشت و متخصصان مجبور بودند بخش اعظم كار را به صورت دستي انجام دهند؛ جز براي برنامه‌هايي كه از لحاظ پيچيدگي نسبتاً معمولي و از لحاظ اهميت بسيار حياتي بودند: مثلاً در الگوريتمي براي كنترل خطوط راه‌آهن، چنين روش‌هاي دشوار و دقيقي غيرعملي مي‌نمود.
در سال‌هاي اخير محققان روش‌ كاملاً متفاوتي ابداع كرده‌اند كه از توانايي پردازنده‌هاي قوي امروزي براي آزمون تمام سناريو‌هاي ممكن بهره مي‌گيرد.

اين روش كه به آن چك‌كردن مدل (Model Checking) مي‌گويند، در حال حاضر به طور گسترده براي بررسي طراحي مدارهاي مجتمع به كار گرفته مي‌شود. ايده اين روش اين است كه هر سلسله از وضعيت‌هاي ممكني را كه يك سيستم در عمل ممكن است با آن روبه‌رو شود بررسي كنيم و مطمئن شويم كه هيچ يك از آن‌ها منجر به شكست سيستم نخواهد شد. منظور از وضعيت (State)، شرايط سيستم در هر زمان مشخص است. براي يك ميكروچيپ تعداد وضعيت‌هايي كه بايد بررسي شود، اغلب بسيار بزرگ است؛ چيزي حدود 10 به توان 100 يا بيشتر! بررسي وضعيت‌ها براي يك نرم‌افزار بسيار دشوارتر است. اما تكنيك‌هاي هوشمندانه‌اي بركدگذاري وجود دارد كه به كمك آن‌ها مي‌توان مجموعه‌هاي بزرگي از وضعيت‌هاي يك نرم‌افزار را به طور خيلي فشرده بيان كرد. با استفاده از اين تكنيك‌ها مي‌توان اين مجموعه‌هاي بزرگ را به طور همزمان بررسي كرد و به اين ترتيب تمام وضعيت‌هاي ممكن يك نرم‌افزار را آزمايش كرد.

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

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

[B O L O T]

راه‌حل، يك پازل است!
براي اين‌كه بفهميد Alloy چطور معماي طراحي نرم‌افزار را حل مي‌كند، بد نيست به يك معماي قديمي اشاره كنيم: يك كشاورز به بازار مي‌رود و يك روباه، يك غاز، و يك كيسه ذرت مي‌خرد. در راه برگشت به خانه، بايد با قايق از يك رودخانه رد شود، ولي قايق در هر بار فقط مي‌تواند او و فقط يكي از خريدهايش را ببرد. مشكل اينجاست كه اگر او نباشد، روباه غاز را مي‌خورد و غاز ذرت را. حالا كشاورز چطور خريد‌هايش را سالم به آن طرف رودخانه ببرد؟

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

در يك طراحي موفق نرم‌افزار هم، چنين قيدهايي وجود دارد، اگرچه بسيار پيچيده‌تر هستند. هدف يك ابزار بررسي طراحي اين است كه مثال‌هاي نقض براي طراحي پيدا كند: يعني راه حل‌هايي براي معما كه با همه قيد‌هاي خوب مطابقت دارند (بنابراين وقتي برنامه اجرا مي‌شود، مي‌توانند اتفاق بيفتند) و علاوه بر آن حداقل با يك قيد بد هم سازگارند (بنابراين مي‌توانند منجر به نتيجه‌اي نامطلوب شوند).

هرگاه يك مثال نقض به اين ترتيب پيدا شود، نشان‌دهنده خطا در طراحي است. بنابراين، اگرچه ابزارِ معماحل كن از پيدا كردن راه حل معماي كشاورز خوشحال مي‌شود، جواب معماي طراحي نرم‌افزار خبر شادي‌بخشي نيست. چون نشان مي‌دهد كه يك سناريوي نامطلوب وجود دارد و طراحي نرم‌افزار ايراد دارد.

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

هدف اين است كه هريك از وضعيت‌هايي را كه نرم‌افزار ممكن است داشته باشد، شبيه‌سازي كنيم تا مطمئن شويم كه هيچ يك منجر به شكست نخواهد شد.



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

اما اگر مثلاً چند نفر از آن‌ها قبلاً با هم دوست بوده‌اند و حالا با هم قهرند، نبايد آن ها را كنار هم نشاند و اين مسئله را سخت‌تر مي‌كند. حالا تصور كنيد كه مهماني عروسي مال رومئو و ژوليت است.(1) اگر فقط بيست صندلي داشته باشيم و هريك از ده نفر مهمان بتواند آزادانه روي هر صندلي كه خواست بنشيند، تعداد تركيب‌هاي ممكن برابر 10 به توان 20 حالت خواهد بود. يك كامپيوتر حتي اگر بتواند در هر ثانيه يك ميليارد سناريو را بررسي كند، باز به سه‌هزار سال وقت براي بررسي همه حالت‌ها نياز دارد.

در دهه 1980، محققان رياضيات مسائلي از اين دست را تحت عنوان كلاس خاصي از مسائل طبقه‌بندي كردند كه در بدترين حالت براي حل آن‌ها بايد تمام حالت‌‌هاي ممكن را تك تك بررسي كرد، ولي در دهه گذشته با ابداع استراتژي‌ها و الگوريتم‌هاي جديد جست‌وجو و افزايش روزافزون قدرت محاسباتي، محققان ابزارهايي به اسم SAT solver (حل‌كننده SAT) ساخته‌اند كه مي‌توانند چنين مسئله‌هايي را نسبتاً به آساني حل كنند.(2) در حال حاضر انواع مختلفي از SAT solverها به صورت رايگان در دسترس هستند كه مي‌توانند مسائلي با ميليون‌ها قيد را حل كنند

[B O L O T]

اهميت انتزاعي عمل كردن‌
Alloy (آلياژ) همان‌طور كه از نامش پيداست، از تركيب دو عنصر براي كمك به قوي‌تر كردن طراحي نرم‌افزار بهره مي‌گيرد. يكي از آن‌ها زبان جديدي است كه به كمك آن مي‌توان ساختار و رفتار نرم‌افزار را توضيح داد. ديگري تحليلگر خودكاري است كه با استفاده از يك SAT solver تمام سناريوهاي ممكن را بررسي مي‌كند.
اولين مرحله در استفاده از Alloy، ساختن يك مدل از طرح نرم‌افزار است.

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

پس از آن، واقعيت‌ها (fact) بيان مي‌شوند كه مجموعه‌ها و رابطه‌ها را محدود مي‌كنند. در طراحي نرم‌افزار واقعيت‌ها شامل مكانيسم‌هاي سيستم نرم‌افزاري و فرض‌هايي درباره ديگر اجزا است (مثلاً گزاره‌هايي درباره رفتار احتمالي كاربران سيستم). بعضي از اين واقعيت‌ها فرض‌هاي واضحي هستند (مثلاً اين‌كه هيچ كس نمي‌تواند هم كاپولت و هم مونتاگو باشد و اين‌كه هر مهمان دقيقاً در كنار دو مهمان ديگر خواهد نشست) و بعضي از آن‌ها از خود طراحي ناشي مي‌شوند؛ براي نمونه در مثال ما، اين قانون كه هر ميز، جز ميز بالا‌ي مجلس، بايد فقط به اعضاي يك خانواده اختصاص داشته باشد.

نهايتاً، حكم‌ها (assertion) قرار مي‌گيرند كه قيدهايي هستند كه از واقعيت‌ها ناشي مي‌شوند.به عنون نمونه در مثال ما، جز رومئو و ژوليت، هيچ كاپولتي نبايد كنار يك مونتاگو بنشيند. حكم‌ها مي‌گويند كه سيستم هرگز نمي‌تواند دچار بعضي وضعيت‌هاي نامطلوب شود و سلسله‌هاي مشخصي از رويدادهاي بد، هرگز نمي‌توانند اتفاق بيفتند.

بخش تحليلگر Alloy براي يافتن مثال‌هاي نقض از يك SAT solver استفاده مي‌كند. مثال‌هاي نقض سناريوهاي احتمالي در يك سيستم نرم‌افزاري هستند كه طراحي سيستم اجازه رخ دادن آن‌ها را مي‌دهد، ولي نمي‌توانند آزمون درستي (sanity check) را پشت سر بگذارند. آزمون درستي با نوشتن حكم‌هايي كه اگر طراحي مدل درست باشد، مقدار آن‌ها درست (True) مي‌شود، انجام مي‌شود. به زبان ديگر، اين ابزار سعي مي‌كند شرايطي را پديد آورد كه با واقعيت‌ها مطابقت دارند، ولي حداقل يك حكم بيان شده را زير پا مي‌گذارند. مثلاً در مثال ما، ممكن است ترتيبي براي نشستن افراد پيدا كند كه طي آن در ميز بالا‌ي مجلس يك كاپولت (غير از ژوليت) كنار يك مونتاگو (غير از رومئو) بنشيند. براي اين‌كه جلوي رخ دادن چنين سناريويي را بگيريم، مي‌توانيم در طرح نرم‌افزارمان يك واقعيت جديد اضافه كنيم: فقط رومئو و ژوليت پشت ميز بالا‌ي مجلس مي‌نشينند. حالا ديگر Alloy نمي‌تواند مثال نقضي پيدا كند.

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

در مقابل، اگر دقت كنيم، مي‌بينيم كه سيستم‌هايي كه در آن‌ها نرم‌افزار بر اساس يك انتزاعي ساده و قوي ساخته شده است، نه تنها قوي‌ترند، بلكه حتي استفاده از آن‌ها هم ساده‌تر است. مثلا ًe-Ticketing را در نظر بگيريد كه چطور مسافرت‌هاي هوايي را راحت‌تر كرده است يا كد جهاني كالا (UPC) كه چطور موجب سهولت فروش شده است، يا تلفن‌هاي معاف از ماليات با پيش‌شماره هشتصد كه تله‌كنفرانس را ساده‌تر ساخته‌اند. در تمام اين نوآوري‌ها شاهد تحولي در انتزاعي هستيم كه نرم‌افزار بر اساس آن ساخته شده است.

[B O L O T]

قابليت اطمينان نرم‌افزارها در آينده‌
در حال حاضر ابزارهايي مثل Alloy بيشتر در تحقيقات و سيستم‌هاي صنعتي فوق پيشرفته به كار گرفته مي‌شوند. اين فناوري براي بررسي معماري‌هاي جديد در سيستم‌هاي سوييچينگ تلفن، براي طراحي پردازنده‌هاي به كار رفته در صنعت هوانوردي و سيستم‌هاي ايمن در مقابل حمله هكرها، و براي وضع سياست‌‌هاي كنترل دسترسي در شبكه‌هاي ارتباطاتي به كار گرفته شده است.

همچنين با استفاده از اين فناوري برخي مكانيسم‌هاي نرم‌افزاري مهم و پر استفاده را نيز بررسي كرديم؛ براي مثال، پروتكل‌هايي كه براي يافتن چاپگرها در شبكه به كار مي‌روند يا ابزارهايي براي همزمان‌سازي فايل‌ها بين كامپيوترهاي مختلف.

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

ابزارهايي مثل Alloy به احتمال زياد در آينده به طور گسترده‌تري در صنعت به كار گرفته خواهند شد. با بهبود SAT solver‌هاي به كار رفته در اين ابزارها، آن‌ها مي‌توانند سيستم‌هاي بزرگ‌تر را بهتر و سريع‌تر بررسي كنند. در عين حال نسل جديد طراحان نرم‌افزار كه با اين روش‌ها آشنايي دارند، از آن‌ها در كار خود استفاده خواهند كرد. در حال حاضر استفاده از مدلينگ رو به گسترش است؛ به‌ويژه از سوي مديراني كه دوست دارند براي توصيف يك نرم‌افزار چيزي بيشتر از كد برنامه آن را ببينند.

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

[B O L O T]

‌منبع: ساينتيفيك‌امريك