عنوان پایان‌نامه
معنا شناسی و تحلیل زبان ریو با منطق رابطه ای
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 42645;کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 1618
- تاریخ دفاع
- ۳۱ شهریور ۱۳۸۸
- دانشجو
- مصطفی زالی
- استاد راهنما
- رامتین خسروی
- چکیده
- چکیده مسأله‌ی هماهنگی بین اجزا امروزه به یک چالش مهم در سامانه‌های همروند تبدیل شده است. تاکنون روش‌های صوری و مدل‌های مختلفی برای مدلسازی سامانه‌های همروند ارائه شده است. ریو یک زبان هماهنگی است که بر اساس مفهوم پیوند شکل گرفته است. پیوند برقراری ارتباط از قبیل انتقال داده و همزمانی میان مؤلفه‌های یک سامانه را بر عهده دارد. این زبان طبیعتی ترکیبی دارد و پیوندهای ریو از ترکیب چند پیوند ساده‌تر ساخته می‌شود. ساده‌ترین نوع پیوند کانال نامیده شده که از جزء ساده‌تری تشکیل نمی‌شود. کانال‌ها می‌توانند با رعایت قواعد خاصی توسط برنامه‌نویس تعریف شوند. معناشناسی‌های صوری برای توصیف دقیق معنای زبان‌های برنامه‌نویسی و یافتن ناسازگار‌ی‌های احتمالی این زبان‌ها به کار می‌روند. تاکنون معناشناسی‌های بسیاری برای زبان ریو مطرح شده‌اند که هر یک فاقد بخشی از قابلیت‌های آن و یا برخی خصوصیات مورد نیاز یک معناشناسی صوری هستند. در این پژوهش، یک معناشناسی جدید مبتنی بر منطق مرتبه‌ی اول رابطه‌ای برای زبان ریو مطرح می‌شود. از خصوصیات این معناشناسی، درنظر گرفتن رفتار حساس به متن، خاصیت ترکیبی بودن - به گونه‌ای که معنای یک پیوند پیچیده از ترکیب معنای دو پیوند سازنده‌ی آن حاصل می‌شود- و نیز سادگی نمادها و قابل فهم بودن است. صحت و سازگاری معناشناسی ارائه شده توسط یک ابزار ماشینی به نام الوی درستی‌یابی می‌شود. همچنین معادل بودن این معناشناسی با معناشناسی جریان داده‌ی زمانمند نشان داده شده است.
- Abstract
- Abstract Coordination among components of a system has become a primary challenge in concurrent systems, and different formalisms and models have been developed for modeling them. Reo is a coordination language based on the concept of connector. A connector establishes the connection, such as data transmission and synchronization, among components of a system. This language has a compositional character and its connectors are constructed out of the composition of simpler ones. The simplest connector is called a channel, which does not consist of any smaller components. Channels can be defined through following certain rules by the programmer. Formal semantics is used to precisely describe the semantics of programming languages and find their probable inconsistencies. Different semantics have been proposed for Reo by now, but they are all lacking in some of Reo capabilities and some attributes required for formal semantics. The first semantics for Reo was proposed based on the concept of timed data streams, and it described a number of special channels of Reo. Another semantics was developed on the basis of operational semantics, and included basic Reo channels as well as an overall description of the system. This semantics has been verified by a tool called Maude. The third semantics was based on the notion of constraint automata and possessed a compositional feature, such that the semantics of a complex connector was obtained through the compositions of semantics of its tow constituent connectors. Another semantics, which was developed by applying graph coloring, was a compositional one that described context-sensitive behavior. In this paper, we present a new semantics for Reo based on first-order relational logic. Some of its key features include the consideration of context-sensitive behavior, its compositional character, simplicity of notations and comprehensibility. We examine the correctness and consistency of our proposed semantics with a verification tool called Alloy. Furthermore, we show the equivalence between this semantics and timed data streams semantics.
