Loading...

Model Checking of Timed Activity Networks

Salehi, Mehdi | 2013

1530 Viewed
  1. Type of Document: M.Sc. Thesis
  2. Language: Farsi
  3. Document No: 44699 (19)
  4. University: Sharif University of Technology
  5. Department: Computer Engineering
  6. Advisor(s): Movaghar, Ali
  7. Abstract:
  8. In recent years, we have seen the proliferation of real-time and time-dependent systems. They have increased both in number and in complexity. Due to their increasing complexity, we need to model them and become assured of their correctness. Several formalisms have been devised for time-dependent systems. They include timed automaton and timed extensions of Petri nets. Our focus is on timed extension of activity networks and its model checking. Activity networksare powerful formalisms which allow designers to model the system in a natural, small and conceivable manner. This way, timed extension of activity networks can greatly help modelers. In this thesis, we propose a method to specify the properties and model check timed activity network, using existing work on timed extension of Petri nets and timed automaton. In our method, the model checking is done by translating the timed activity network to a timed automaton. In addition, we have developed a tool which works with the aforementioned method, and is introduced here. We will also have a comparison between timed activity networks and other similar models. Finally, we demonstrate the method and the tool using several examples and case studies
  9. Keywords:
  10. Model Cheking ; Time Petri Networks ; Time Activity Networks ; Real Time System ; Time-Dependent Systems

 Digital Object List

 Bookmark

  • فصل 1 مقدمات
    • 1-1 وارسی مدل
    • 1-2 مدل‌ها
    • 1-3 سیستم‌های زمانی
    • 1-4 ساختار پایان‌نامه
  • فصل 2 پیش‌زمینه‌ها
    • 2-1 خودکاره‌ی زمانی
    • 2-2 سیستم گذار زمانی
    • 2-3 شبکه‌ی پتری
    • 2-4 منطق‌های زمانی
      • 2-4-1 منطق‌های زمانی درختی
      • 2-4-2 منطق‌های زمانی روی مسیر
    • 2-5 ابزارهای وارسی مدل خودکاره‌ی زمانی
  • فصل 3 کارهای پیشین
    • 3-1 مقدمه
    • 3-2 گسترش شبکه‌ی پتری با زمان
    • 3-3 جی‌تی‌پی‌ان
    • 3-4 شبکه‌ی فعالیت
    • 3-5 ابزارهای وارسی مدل گسترش‌های زمانی شبکه‌ی پتری
  • فصل 4 مدل شبکه‌ی فعالیت زمانی
    • 4-1 تعریف شبکه‌ی فعالیت زمانی
    • 4-2 معنای شبکه‌ی فعالیت زمانی
    • 4-3 فضای حالت شبکه‌ی فعالیت زمانی
    • 4-4 منطق مورد استفاده برای شبکه‌ی فعالیت زمانی
    • 4-5 مقایسه‌ی مدل شبکه‌ی فعالیت زمانی با دیگر مدل‌ها
      • 4-5-1 مقایسه با خودکاره‌ی زمانی
      • 4-5-2 مقایسه با خانواده‌ی پتری گسترش‌یافته با زمان
      • 4-5-3 مقایسه با دیگر تعریف شبکه‌ی فعالیت زمانی
  • فصل 5 روش وارسی مدل و ابزار پیاده‌سازی‌شده
    • 5-1 روش وارسی مدل شبکه‌ی فعالیت زمانی
    • 5-2 معرفی ابزار
    • 5-3 معماری ابزار
    • 5-4 یک نمونه از ورودی و خروجی ابزار
    • 5-5 نمونه‌ای برای بررسی فضای حالت
  • فصل 6 مقایسه و ارزیابی
    • 6-1 مقدمه
    • 6-2 بررسی شرایط وارسی مدل
    • 6-3 بررسی ابزار
    • 6-4 مطالعه موردی
      • 6-4-1 مساله‌ی گذر قطار
      • 6-4-2 زمان‌بندی یک سیستم محاسباتی توزیع شده
  • فصل 7 جمع‌بندی و کارهای آینده
    • 7-1 جمع‌بندی
    • 7-2 کارهای آینده
  • مراجع
  • واژه‌نامه
...see more