عنوان پایان‌نامه
ارائه یک چهار چوب چند عامله جدید با روش های رسمی کاربرد در زنجیره تامین وشبکه ژنی
- رشته تحصیلی
- مهندسی کامپیوتر- آلگوریتم ها و محاسبات
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه پردیس یک فنی شماره ثبت: 4.;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 40493
- تاریخ دفاع
- ۳۰ بهمن ۱۳۸۷
- دانشجو
- زهرا زمانی
- استاد راهنما
- علی معینی
- چکیده
- سیستم های چندعامله راه حلی برای سیستم های پیچیده و توزیع شده امروزی هستند. استفاده از روش های استاندارد طراحی پیش از عملیاتی کردن این سیستم ها از اتلاف هزینه ها و منابع جلوگیری می کند. به همین منظور یک چارچوب کاری جدید برای این سیستم ها طراحی شده و برای اطمینان از صحت آن در عمل، این چارچوب به طور رسمی توصیف و وارسی شده است. مزیت استفاده از روش های رسمی در اثبات فرضیه قوی نهفته در این روش ها می باشد. چارچوب انتزاعی پیشنهاد شده ابتدا در دو کاربرد عملی استفاده می شود. در کاربرد زنجیره تامین این چارچوب امکان اتوماتیک نمودن پروسه پرداخت را در زنجیره تامین فراهم می کند. این سیستم با روش های نیمه رسمی UML توصیف شده و سپس با ابزارهای وارسی و با زبان منطق زمانی صحت آن بررسی می شود. در کاربرد شبکه ژن، داده های بیان ژن در این چارچوب طی مراحلی آنالیز شده و نتایج مورد نیاز کاربر حاصل می شود. برای صحت این چارچوب از نظر امنیت و پیشرفت آن در کلیه مراحل اجرا، سیستم به طور رسمی توصیف و وارسی شده است. نتایج وارسی رسمی این دو سیستم نشان دهنده صحت این دو سیستم و از آن مهمتر تعریف یک چارچوب رسمی درست و امن برای استفاده در زمینه های مشابه می باشد.
- Abstract
- Multi-agent systems are a new solution to the complexity and distributing properties of software. Using standard design methods before implementing the actual system can prevent consuming resources. With this aim, a new framework has been designed for these systems and to ensure its correctness, this framework is specified and verified formally. The advantage of using formal methods is in its strong proof background in theory. The proposed abstract framework is adopted for two different applications. In the supply chain application, this framework can automate the payment process in the supply chain. This system is then specified using the semi-formal language UML, and then verified using the Temporal Logic language. In the gene network application, gene expression data is analyzed using different processes in this framework and the result is then available to the user. To make sure this system is safe and progresses in time, this framework is specified and verified using formal methods. To verify these systems, the SPIN model checker is used and verification results show that this framework is correct and safe to use for further application.
