مهندس وحید رافع (دانشجوی دوره دکتری مهندسی کامپیوتر- نرمافزار)، 14 اسفند از رساله دکتری خود با عنوان «پالایش و تحلیل رفتاری مدلهای مستقل از سکوّ» به راهنمایی دکتر عادل ترکمان رحمانی دفاع کرد. چکیده رساله: امروزه، یکی از فرآیندهای مهم در تولید نرمافزار پالایش مدل است. اما نکته مهم در این فرآیند، پالایش خودکار این مدلهاست، چرا که تولید غیر مکانیزه آنها، ممکن است همراه باخطا بوده و یا حتی امکانپذیر نباشد. همچنین، اطمینان از صحت مدلهایی که در فرآیند پالایش تولید میشوند، به خصوص مدل اولیهای که مبنای پالایش است، بسیار مهم است. وجود خطا به ویژه در سیستمهای حساس باعث ضررهای جانی و مالی میشود. برای تولید خودکار نرمافزار و همچنین اطمینان از صحت آن، استفاده از روشها و زبانهای صوری برای بیان مدلها ضروری میباشد. لذا روش ارائه شده در این رساله نیز صوری بوده و مبتنی بر سیستمهای تبدیل گراف میباشد. در این رساله، با استفاده از سیستمهای تبدیل گراف، روش مناسبی برای پالایش خودکار مدل های مستقل از سکو، به منظور تولید مدلهای وابسته به معماری سرویسگرا،ارائه دادهایم. در این روش،ابتدا یک چارچوب مناسب، به صورت یک الگو، برای هر سطح از انتزاع در نظر گرفتهایم. این چارچوب شامل فرامدل سیستم است که در قالب گراف نوع، مدل شده است. بعلاوه خصوصیات رفتاری اجزاء و قطعات سیستم که شامل مکانیزمهای ارتباطی میان قطعات و پیکربندیهای سیستم است. سپس وضعیت سیستم، در قالب یک گراف میزبان مدل میشود و این مدل، براساس روش ارائه شده، به صورت خودکار پالایزش میشود، تا در نهایت، مدلی که دارای جزئیات معماری سرویس گرا است، بدست آید. در ادامه، صحت روش ارائه شده را،براساس خصوصیات صوری روشهای تبدیل گراف، بررسی و اثبات نمودهایم. در ادامه، برای درستییابی مدلهای بدست آمد و با توجه به اینکه روشهای موجود برای درستییابی سیستمهای تبدل گراف، کارایی لازم را ندارند، با استفاده از تکنیک وارسی مدل، چارچوبی طراحی کردهایم تا توسط آن، بتوان مدلهای بدست آمده را بررسی کرد و از صحت آنها مطمئن شد. نتایج آزمایشات نشان میدهد که روش ارائه شده در مقایسه با روشهای موجود،دارای قابلیت مناسبتری است. سپس، با استفاده از تکنیک ارائه شده برای وارسی سیستمهای تبدیل گراف، چگونگی تحلیل رفتارهای مختلف در قالب سناریوهایی که به صورت ویژگیهای متفاوت (مانند ویژگی دسترسپذیری) ارائه شدهاند را بیان کردهایم. |