بخشی از مقاله
خلاصه
یک سیستم همروند مجموعهای است از فرآیندهایی که به طور همروند اجرا میشوند و در حین اجرا با یکدیگر در تعامل می-باشند. پیچیدگی این سیستمها موجب شده توصیف آنها امری دشوار و مستعد خطا باشد. روشهای صوری، روشهایی هستند مبتنی بر ریاضیات، که میتوانند در تمام دورههای چرخه حیات یک سیستم نرمافزاری اعمال شوند و مبنای ریاضی آنها باعث افزایش دقت و رفع ابهام میشود.
بنابراین استفاده از این روشها برای توصیف سیستمهای همروند میتواند منجر به کاهش خطا و کاهش پیچیدگی این سیستمها شود. تا کنون ابزار و روشهای مختلفی برای استفاده از روشهای صوری در توصیف سیستمهای همروند معرفی شده است که در این مقاله تعدادی از این روشها معرفی میشوند و در انتها یک دسته بندی کلی از این روشها به همراه جنبههای مختلفی از سیستمهای همروند که در هر روش به توصیف آن پرداخته شده است،ارائه میشود.
.1 مقدمه
یک سیستم نرمافزاری را میتوان به عنوان مجموعهای از اجراها در نظر گرفت به گونهای که هر اجرا نمایش دهنده یکی ار رفتارهای سیستم است. به طور کلی دو نوع اجرا در سیستمهای نرمافزاری تعریف میشود: اجرای همروند1 و اجرای لایهای.2 در مدلهای اجرای لایهای یک اجرا در یک حالت اولیه متمایز و ثابت آغاز میشود و به صورت گام به گام در بین حالتهای میانی حرکت میکند و پردازش مورد نظر را انجام میدهد. هر یک از این گامها یک رویداد - یعنی وقوع یک عمل در یکی از مولفههای سیستم - را شرح می-دهد. به عنوان مثال یک سیستم تولیدکننده و مصرفکننده را در نظر بگیرید. فرض میکنیم p، s، r و c به ترتیب نشاندهنده عملیات تولید، ارسال، دریافت و مصرف باشند.
تفاوت این دو حالت در ترتیب وقوع iمین رویداد مصرف و i+1مین رویداد تولید است. در واقع این دو رویداد به صورت مستقل رخ میدهند. بنابراین اجراهای لایهای، رویداد مستقلی را نشان میدهند که به هر ترتیبی میتواند رخ دهد. اما در اجراهای همروند، ایده اصلی اجتناب از اجرای لایهای دلخواه و غیرقانونمند رویدادهای مستقل است. به عنوان مثال فرض کنید در یک سیستم تولید-کننده و مصرفکننده رفتار سیستم تولیدکننده به صورت شکل 3 می باشد یعنی i مین رویداد ارسال، بعد از iمین رویداد تولید و قبل از i+1مین رویداد تولید، رخ میدهد؛ و به طور مشابه رفتار سیستم مصرفکننده به صورت شکل 4 است . با فرض وجود بافری که حداکثر یک عنصر را ذخیره میکند شکل 5 یک اجرای همروند را در این سیستم نشان میدهد به طوری که iمین رویداد دریافت بعد از iمین رویداد ارسال و قبل از i+1مین رویداد ارسال رخ میدهد .[1]
روشهای همروند نخستین بار در شبکه های پتری3 تعریف شدند [1]، اما در سالهای اخیر، با استفاده رو به افزایش روشهای همروند در سیستمهای کامپیوتری مواجه بودهایم. در یک بیان ساده یک سیستم همروند مجموعهای است از فرآیندهایی که به طور همروند اجرا میشوند و با یکدیگر در تعامل میباشند که این تعامل بر اساس همکاری یا رقابت انجام میشود .[2] به عنوان مثال رشتهها 4 - که فرآیندهای سبکوزن نامیده میشوند - را میتوان به عنوان نمونهای از فرآیندهای همکار به شمار آورد که این همکاری موجب افزایش همروندی میشود. به طور کلی یک سیستم همروند حالتهای اجرایی بسیاری دارد و همین امر باعث شده توسعه این سیستمها یک کار پیچیده و مستعد خطا باشد.
بنابراین استفاده از روشهای صوری5 در توصیف این سیستمها میتواند مفید واقع شود و باعث کاهش پیچیدگی و خطا شود. در واقع میتوان گفت به کارگیری روشهای صوری در توصیف سیستمهای همروند میتواند باعث افزایش سطح ایمنی و صحت برنامههای نهایی شود .[2] روش صوری، تکنیکی است که از مفاهیم ریاضی برای توصیف، درستی یابی یا تولید برنامهها استفاده میکند و در نتیجه به کارگیری روشهای صوری در مراحل مختلف توسعه نرمافزار میتواند منجر به افزایش دقت و رفع ابهام شود .[2] در یک توصیف صوری هدف اصلی تشریح یک سیستم نرمافزاری به گونهای ساده و قابل درک میباشد .[3]
تا کنون توصیفهای صوری بسیاری برای سیستمهای همروند با استفاده از روشها و زبانهای مختلف مثل [4] Z، [5] CSP، [6] CCS، [7] XCCS و ... ارائه شده است اما تنها تعداد کمی از این روشها در توصیف جنبههای مهم این سیستمها مثل تولید فرآیند پویا، زمانبندی، گرسنگی و ... موفق بودهاند. در این مقاله به معرفی تعدادی از این روشها و ویژگیهای هر یک میپردازیم و در نهایت یک دستهبندی کلی از این روشها ارائه میدهیم.
در بخش 2 به معرفی زبانهای Z، Object-Z و CSP میپردازیم که در اکثر روشهای توصیف معرفی شده در اینجا مورد استفاده قرار گرفته اند. سپس در بخش 3 همترین خصوصیات یک سیستم همروند را تعریف میکنیم. بخش 4 شامل شرح 7 روش ارائه شده در مقالههای مختلف برای توصیف سیستمهای همروند میباشد علاوه بر این در این بخش به مقایسه روشهای مختلف توصیف سیستمهای همروند پرداختهایم و نتاج در قالب یک جدول نشان داده شده است.در نهایت در بخش 5 نتیجه حاصل از این بررسی بیان شده است.
2 معرفی چند زبان توصیف صوری
در این بخش به معرفی مختصر سه زبان صوری که در اکثر روشهای معرفی شده در این بخش مورد استفاده قرار گرفتهاند میپردازیم.
.1,2 زبان Z
زبان Z یکی از زبانهایی است که برای توصیف صوری سیستمهای نرمافزاری به کار میرود. این زبان مبتنی بر تئوری مجموعهها و منطق مسندات مرتبه اول است به طوری که ترکیب این دو مفهوم باعث ایجاد یک زبان مبتنی بر ریاضیات شده که یادگیری و به کارگیری آن، ساده میباشد .[2] در این زبان از ساختارهای توصیفی مثل - تعاریف اصول بدیهی6 و شما - 7 برای مدلسازی حالت و رفتار سیستم استفاده میشود.
در این میان، شما مهمترین ابزار برای کپسولهسازی بخشهای مختلف توصیف است. این ساختار، هم برای مدلسازی حالت سیستم - به عنوان شمای حالت - 8 و هم برای مدلسازی رفتار سیستم - به عنوان شمای عملیاتی - 9 مورد استفاده قرار میگیرد .[2] ساختار ساده و مبتنی بر ریاضیات زبان Z موجب شده به طور گسترده برای توصیف صوری سیستمهای نرمافزاری از جمله سیستمهای همروند مورد استفاده قرار گیرد.
.2,2 زبان Object-Z
زبان Object-Z شکل توسعه یافتهای از زبان Z است که برای توصیفهای شیگرا طراحی شده است. این زبان شامل یک ساختار تعریف کلاس است که یک شمای حالت را به همراه تمام عملیات مربوط به این شما، کپسوله میکند. یک کلاس ممکن است برای تعریف یک یا چند مولفه سیستم یا برای تعریف تعامل بین مولفههای سیستم مورد استفاده قرار گیرد .[3] در object-Z یک کلاس به صورت یک جعبه نامگذاری شده نشان داده میشود که شامل انواع متغیرهای محلی و تعریفهای ساختاری به اضافه حداکثر یک شمای حالت اولیه و صفر یا چند شمای عملیاتی است. شکل 6 مثالی از یک کلاس صف با اندازه محدود را نشان میدهد .[3]
علاوه بر این امکان تعریف وراثت که یکی از خواص سیستمهای شیگرا میباشد نیز در object-Z وجود دارد. در این حالت انواع متغیرهای محلی و ساختارهای تعریف شده در یک کلاس والد، به طور صریح در کلاس فرزند نیز قابل دستیابی هستند. شماهای تعریف شده در کلاس والد نیز در کلاس فرزند قابل دستیابی هستند مگر در مواقعی که در کلاس فرزند شمایی با همین نام تعریف شده باشد. شکل 7 مثالی از یک کلاس صف را نشان میدهد که از کلاس صف تعریف شده در شکل 6 به ارث میرسد .[3]
.3,2 زبان CSP
CSP، زبانی است که به طور اختصاصی برای توصیف سیستمهای همروند طراحی شده است. این زبان یک سیستم همروند را به صورت مجموعهای از فرآیندها مدل میکند که به طور همروند اجرا میشوند و از طریق مجموعهای از کانالها با هم در ارتباط هستند و در برخی رویدادها همزمان میباشند. در CSP فرآیندها به وسیله معادلات خاص و معمولا به صورت بازگشتی توصیف میشوند. به عنوان مثال یک بافر one-place ساده می تواند به صورت نشان داده شده در شکل 8 توصیف شود .[3]
برای ترکیب فرآیندهای مختلف، CSP از تعدادی عملگر استفاده میکند. یکی از مهمترین عملگرها، عملگر همروندی است. وقتی دو فرآیند با استفاده از این عملگر با هم ترکیب میشوند بدین معناست که این دو فرآیند به طور همروند اجرا میشوند و روی رویدادهای همنام به صورت همزمان اجرا میشوند و اگر رویدادها از نوع رویدادهای ارتباطی باشند روی رویدادهایی با نام و مقدار کانال یکسان همزمان میشوند.
