دفاعیه دکتری در دانشکده مهندسی کامپیوتر

   مهندس وحید رافع (دانشجوی دوره دکتری مهندسی کامپیوتر- نرم‌افزار) 14 اسفند ماه از رساله دکتری خود با عنوان «پالایش و تحلیل رفتاری مدل‌های مستقل از سکو» به راهنمایی دکتر عادل ترکمان رحمانی دفاع کرد.

  چکیده رساله:

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

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

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

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

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

  در انتها، با استفاده از تکنیک ارائه شده برای بررسی سیستم‌های تبدیل گراف، چگونگی تحلیل رفتارهای مختلف در قالب سناریوهایی که به صورت ویژگی‌های متفاوت (مانند ویژگی دسترس‌پذیری) ارائه شده‌اند را بیان کرده‌ایم.