بخشی از مقاله
معرفی روش صوری WDM و کاربرد آن در مهندسی نرم افزار
چکیده
در یک دهه اخیر استفاده از روش های صوری جهت توسعه سیستم های قابل اعتماد به شدت فزونی یافته است. در نتیجه روش های صوری متعددی ارائه شده اند که هر یک کاربردهای خاصی همچون توسعه سیستم های همروند، توزیع شده، بلادرنگ و غیره دارند. مفهوم روشهای صوری تعداد بی شماری از تکنیکهای علمی را برای مدلسازی و کنترل بسیار دقیق سیستمهای جهان واقعی توصیف می نماید. یکی از قدیمیترین روشهای صوری اثبات شده جهت توسعه سیستمهای مبتنی بر کامپیوتر، روش صوری WDM است. در این مطالعه، به معرفی روش صوری VDM، زبان مشخصات WDM-SL و تحقیقات انجام شده در زمینه کاربرد آنها در مهندسی نرم افزار پرداخته شده است.
۱- مقدمه
یکی از راه های پیشرفت و بهبود کیفیت نرم افزار، ایجاد تغییرات در مرحله طراحی، در طول توسعه و بعد از انتشار نرم افزار مستندسازی شده می باشد. روش های مستندسازی موجود شامل مقادیر زیادی متن، عکس و دیاگرام هستند. اما این موارد اغلب غیر دقیق و مبهم می باشند || ۱ || اطلاعات مهم در میان جزئیات نامربوط مخفی می شوند و عیوب و اشکالات طراحی خیلی دیر کشف می شوند، لذا اصلاح آنها غیر ممکن است و یا گران تمام می شود] ۲].
یک روش دیگر در مقابل چنین روشی، استفاده از روش های صوری است که منجر به تولید مستندات دقیق و نامبهم می شود. با استفاده از این روش اطلاعات لازم ساخت یافته می شوند و در یک سطح مناسب از انتزاع ارائه می گردند. چنین مستنداتی می تواند برای پشتیبانی فرایندهای طراحی و به عنوان یک راهنما جهت توسعه های بعدی، آزمایش و نگهداری نرم افزار مورد استفاده قرار گیرد [۱].
۲- روش های صوری اصطلاح روشهای صوری شامل فعالیتهای مختلفی از جمله تعیین مشخصات صوری، تحلیل و اثبات مشخصات، توسعه تبدیلی و وارسی برنامه است. تمام این فعالیت ها به مشخصات صوری نرم افزار بستگی دارند. مشخصات صوری نرم افزار، مشخصاتی است که به زبانی بیان شده است که واژگان، نحو و معنای آن به طور صوری تعریف شدهاند. نیاز به تعریف صوری به معنای این است که زبانهای تعیین مشخصات باید بر اساس مفاهیم ریاضی باشند. روشهای صوری از ریاضیات برای توسعه نرمافزار استفاده می نمایند] ۳[ و مفاهیم ریاضی از تئوری مجموعه، منطق و جبر گرفته شده است ] ۴ [تا تضمین نماید
مشخصات مختصر و دقیق به دست آید ]۵[
همچنین این روش ها یک زبان صوری برای بیان صریح خصوصیات اصلی و ابتدایی و همه مراحل طراحی، تا رسیدن به برنامه نهایی، ارائه میکنند. علاوه براین، روشهای صوری شامل یک سیستم قطعی است، یک سیستم قطعی به معنای ضمانت درستی یک عبارت است و به منطق ریاضی مربوط می شود، به این ترتیب ثابت میگردد که برنامه نهایی با خصوصیات اصلی و ابتدایی سازگار است ]۲].
روش های صوری به طور فزایندهای در توسعه سیستم های بحرانی به کار گرفته می شوند که در این سیستم ها ویژگیهایی نظیر ایمنی، قابلیت اعتماد و امنیت بسیار مهم هستند. هزینه بالای شکست در این سیستمها به معنای این است که شرکت ها میخواهند هزینه های بالای روش های صوری را بپذیرند تا مطمئن شوند که نرم افزار آنها قابل اتکا است ]۴ [
۲- ۱- دسته بندی روش های صوری
روشهای صوری، داده گرا، فرایندگرا و یا عملیات گرا می باشند ] ۶ [ که بر همین اساس نیز آنها را به دو دسته عمده طبقه بندی می کنند [۴ و ۲]
الف) روش جبری که در آن سیستم برحسب عملیات و روابط توصیف میشود. به عبارت دیگر، لیستی از عملکردهای مطلوب به یکباره، شناسایی می شوند و رفتار آنها به طور غیرمستقیم و به وسیله تشریح روابط بین این عملکردها، به عنوان مجموعه ای از ویژگی ها نشان داده میشود. همه نرم افزارهایی که توسط این روش توسعه داده شده اند باید ثابت کنند که ویژگی هایشان با خصوصیات تعیین شده مطابقت می کند.
ب) روش مبتنی بر مدل که در آن با استفاده از ساختارهای ریاضی مثل مجموعه ها و دنباله ها مدلی از سیستم ساخته و عملیات سیستم برحسب چگونگی اصلاح حالت سیستم تعریف می شوند. عملیات موجود در مشخصات مبتنی بر مدل، با تعریف پیش شرطها و پس شرطها روی حالت سیستم مشخص میگردند. معمولاً این روش، خصوصیات را خیلی مختصرتر از روش جبری به دست می آورد. روش های داده گرا و فرایندگرا در این دسته هستند.
روش های صوری مختلفی وجود دارند اما هدف نهایی همه آنها یکسان است. برخی از این روشها برای تعیین خصوصیات سیستمهای ترتیبی مناسبتر هستند، در حالی که برخی از روشهای دیگر برای سیستمهای همروند به کار می روند. جدول ۱، دسته بندی روش های صوری را براساس این تفاوت نشان میدهد.
معمولترین و قابل قبول ترین روشهای صوری آن هایی هستند که مدل گرا بوده و برای سیستمهای ترتیبی ارائه شده اند. یکی از دلایل آن این است که استفاده از روشهای مدل گرا راحتتر است؛ زیرا آنها بر مبنای درک شهودی ما از سیستمها به صورت مخزنی از دادهها و مجموعه ای از عملکردها طرحریزی شده اند. علاوه براین، توصیف سیستمهای همروند نیازمند ملاحظات زمانی دقیق است که درک آنها به صورت صوری معمولاً آسان نیست ]۲].
۲- ۲- کاربرد روش های صوری روش های صوری در حوزه های مختلفی به کار گرفته می شوند که می توان در رده های زیر خلاصه نمود ]۱[
استفاده در تئوری احتمالات برای کارایی مدل سازی
استفاده در گرامرهای مستقل ازمتن جهت طراحی کامپايلرها
استفاده در حساب رابطه ای موجود در تئوری پایگاه دادهها
استفاده در تعیین مشخصات و طراحی بسیاری از سیستم های نرم افزاری
سیستم های بحرانی که روش های صوری در آنها با موفقیت انجام شد شامل سیستم اطلاعات کنترل ترافیک هوایی، سیستمهای سیگنال دهی راه آهن، سیستم های فضانوردی و سیستمهای کنترل پزشکی میباشند [۴].
3- روش VDM
یکی از قدیمی ترین روش های صوری اثبات شده جهت توسعه سیستم های مبتنی بر کامپیوتر، روش VDM است. VDM یک زبان صوری توسعه یافته در آزمایشگاه IBM در Vienna می باشد که شامل مجموعه ای از تکنیک ها برای مدلسازی، تعیین مشخصات و طراحی سیستم های کامپیوتری است [۸و۷].
در سال های ۱۹۷۰، VDM بیشتر برای توصیف زبان برنامه سازی و طراحی کامپایلر به کار گرفته می شد و هدف اصلی آن توسعه ویژگی های بنیادی زبان و بیان و اثبات برخی قواعد معنایی صوری محسوب می شد || ۷ || یکی از نخستین کاربردهای جالب توجه VDM، تلاش جهت به دست آوردن یک تعریف صوری برای قواعد معنایی زبان PL/I بود. نشانه گذاری های به کار رفته در این روش VDL نامیده می شد ] ۹ و ۸و۷].
اثبات ها نیز یکی از موضوعات مورد بحث در گروه Vienna بود به همین دلیل VDM برای اثبات هم ارزی مفاهیم زبان برنامه سازی به عنوان قسمتی از مبحث صحت کامپایلر استفاده می شد. در این مرحله جنبه های متفاوت بیشماری از این مباحث مورد بررسی قرار گرفت. اگر چه دغدغه هایی درباره کیفیت و سبک اثبات ها وجود داشت، اما رسمی سازی کامل به طور واقعی در آن زمان مورد نیاز نبود، تا اینکه ابزارهای پشتیبانی امکانپذیر گشته و در دسترس قرار گرفتند ] ۷ [
در سال ۱۹۷۵ گروه Vienna پراکنده شدند که این امر متعاقباً منجر به رهیافت های متفاوت در توسعه های بعدی شد، به طوریکه زبان مدل سازی، متدولوژی و تکنیک های وابسته به اثبات در چندین راستا و با دستورات مختلف گسترش یافتند. در سال ۱۹۸۰، VDM با انتقال از "تعریف زبان" به یک "روش توسعه " مورد آزمایش قرار گرفت و بیشتر استاندارد شد و کامل گردید [۷].
از بین روش های مدل گرا که برای توسعه سیستم های ترتیبی لیست می شود، VDM تکامل یافته تر است ] ۲ [ این زبان صوری همچنین دارای مجموعه ای جامع از ابزارهای پشتیبانی کننده می باشد و از آنجا که یکی از قویترین روش های صوری شناخته شده است، بیشترین سابقه استفاده در صنعت را هم دارد ]۱۰ و ۷ و ۶[. از میان بقیه روش ها، روش B و Z در حال حاضر، در کارهای صنعتی که خوب مستندسازی شده اند استفاده می شوند. آنها شباهت زیادی به VDM دارند اما به اندازه آن تکامل یافته نیستند [۲].
-1-3روش ++ VDM
یک زبان مشخصات شی گرا و یک شاخص از مVDM-SL می باشد. در این روش، VDM از کلاس ها برای توصیف مشخصات مدل ها استفاده می کند ] ۱۲ و ۱۱[ . یک کلاس ++VDMi شامل چندین قسمت است. متغیرهای نمونه، عملیات و توابع در آغاز کلاس معرفی می شوند] ۷ [. همچنین در این روش امکانات استفاده از نخ ها برای ارتباط اشیاء مشترک فراهم شده است ]۱۱]. در بخش نخی و همگام سازی یک کلاس رفتارهای همروند نیز می توانند به راحتی تعیین شوند || ۱۲]. طرح کلی کلاس در ++VDM در شکل ۱ نشان داده شده است.
-2-3زبان VDM-SL
یک استاندارد به رسمیت شناخته شده بینالمللی توسط ISO دارد که معناشناسی زبان صوری را ارائه میدهد و به اختصار VDM-SL نامیده می شود ]۱۰ و ۸و۷]. هر مشخصاتی که برای یک سیستم بیان می شود برای اینکه به زبان صوری VDM-SL نوشته شود می بایست درون یک قالب استاندارد قرار گیرد. این الگوی کلی در شکل ۲ نشان داده شده است. در ادامه هر یک بخش های مربوط به الگوی شکل ۲ به اختصار بررسی می شود
۳- ۱-۲ انواع تعریف شده توسط کاربر
اولین جزئی که در تعیین مشخصات ذکر می شود مشخص نمودن انواع تعریف شده توسط کاربر می باشد. انواع از پیش تعریف شده که در طول مشخصات مورد نیاز خواهند بود، به همراه اجزای سازنده خود پس از کلمه کلیدی type قرار می گیرند و توسط دو نقطه (:) از یکدیگر جدا می شوند] ۲ [
علاوه بر این، نوع منحصر به فردی در VDM-SL به نام تعریف می شود که چنانچه نیاز باشد سخت افزار کار خاصی را انجام دهد، در صورت برآورده شدن شرایط، عمل مورد نظر با فراخوانی رخ می دهد ] ۲ |[یکی دیگر از
