عنوان پایان‌نامه
درستی یابی صوری سیستمهای شی بنیاد توسط جبر پردازه ای
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 36700;کتابخانه دانشکده برق و کامپیوتر شماره ثبت: E 1364
- تاریخ دفاع
- ۲۳ آبان ۱۳۸۶
- استاد راهنما
- مرجان سیرجانی
- دانشجو
- حسین حجت
- چکیده
- الگوی مبتنی بر شیء یکی از رایج‌ترین رویکردها به برنامه‌سازی و مدل‌سازی است. باوجود اینکه پیشرفت‌های بسیاری در این زمینه انجام شده است، اما به نظر می‌رسد که هنوز این الگو نظریات پخته و جاافتاده‌ای برای استدلال صوری نداشته باشد. در این پایان‌نامه تلاش می‌کنیم که پایه‌ای برای استدلال صوری در زمینه‌ی زبان‌های مبتنی بر شیء بنا کنیم. برای تحلیل صوری، از شیوه‌ی تحلیل جبرپردازه‌ای استفاده می‌کنیم، که رویکردی قدرتمند برای مدل‌سازی سیستمهای همروند است. با فراهم کردن نگاشتی از زبان‌های مبتنی بر شیء به جبرپردازه‌ای، می‌توانیم از توانمندی‌های جبرپردازه‌ای در کاربردهای صنعتی نیز استفاده کنیم. در نگاشت ارائه شده به طور خاص بر جبرپردازه‌ای mCRL2 تمرکز می‌کنیم، که یک شکل از جبرهای پردازه‌ای است که از انواع داده‌ای به خوبی پشتیبانی می‌کند. توانایی‌های mCRL2 در کارهای بسیاری پیش از این به اثبات رسیده بودند، و علاوه‌براین مجموعه ابزارهای نیرومندی برای تحلیل و درستی‌یابی مدل‌های mCRL2 وجود دارند. برای عملی کردن ایده‌های خود از دو زبان مبتنی بر شیء استفاده می‌کنیم. اولی زبان ربکاست، که زبانی مبتنی بر مدل بازیگر است که برای مدل‌سازی سیستمهای همروند و توزیع‌شده به کار می‌رود. زبان دوم زبان SystemC است که در صنعت کاربرد بسیار دارد. این زبان در طراحی‌های در سطح سیستم کاربرد دارد. برتری‌های رویکرد ما در مقایسه با نگاشت‌های انجام شده‌ی پیشین در زمینه‌ی تبدیل زبان‌های مبتنی بر شیء به جبرپردازه‌ای، استفاده‌ی بسیار از انواع داده‌ای موجود در mCRL2 است. توانایی انواع داده‌ای موجود در mCRL2 تاحدی بود که عموماً نیازی به تعریف مجدد انواع داده‌ای احساس نشد. هر دو نگاشت در قالب یک ابزار کامپایلر پیاده‌سازی شده و تعدادی مطالعه‌ی موردی در هر دو مورد انجام شده‌اند. نتایج نگاشت ربکا نشان می‌دهد که کاهش ترتیب جزئی پویا اندازه‌ی فضای حالت را نسبت به روش‌های پیشین (که ایستا بودند) بیشتر کاهش می‌دهد، حال آنکه از لحاظ زمانی کُندتر است. همچنین توانستیم که یک اشکال در پیاده‌سازی انجام شده‌ی قبلی برای روش‌های ایستای کاهش ترتیب جزئی بیابیم، که توسط خوشه‌سازی قابل حل شدن است. در نگاشت SystemC نیز یک اشکال مخفی در پیاده‌سازی ریزپردازنده‌ی mini MIPS پیدا شد، که تا قبل از آن یافته نشده بود.
- Abstract
- The object paradigm has been recognized as one of the most popular approaches to modeling and programming. However, despite the remarkable advancements it seems that the paradigm still lacks established formal treatment theories. In this thesis, we are to provide a basis for formal reasoning on the object based languages. We pick process algebraic style of formal analysis, which is a powerful approach to the modeling of concurrent systems. By providing a mapping from object based languages to process algebra, we can utilize the capabilities of process algebra in real case studies coming from industry and commerce. We purposely use mCRL2, which is a process algebra enhanced with data types. The potentials of mCRL2 have been proven in numerous earlier experiments, and moreover there is a powerful toolset for analysis and verification of the mCRL2 models. In order to materialize our ideas we select two object based languages. The first one is Rebeca, an actorbased language for modeling concurrent and distributed systems. The the second one is from industry, SystemC, exploited for the system-level designs. The main advantage of our approach in comparison with the earlier mappings of object based languages to process algebra is our extensive use of the built-in data types of mCRL2 and avoiding the redefinition of our own set of data types. Both mappings have been implemented as a compiler, and a number of case studies have been checked in either case. The results of the Rebeca mapping explains that the dynamic partial order reduction can decrease the size of the state space more than the previous used static partial order methods, while it is slower and more time consuming. We could also find a deficiency in the static version of our partial order reductions, which can be solved by clustering. In the case of the SystemC mapping we found and recovered a hidden bug in the implementation of a mini MIPS processor which was not discovered before.
