1390

استفاده از بررسي مدل در سيستم هاي کنترل ترافيک: يک کاربرد عملي

طراحی و پیاده‌سازی سیستم‌های کنترل حمل و نقل به واسطه‌ی نقشی که در رفع ازدحام ترافیک شهرها ایفا می‌کرده‌اند از دیرباز از اهمیت خاصی برخوردار بوده است. در این راستا، پروژه‌های عملی زیادی تعریف و سیستم‌های متعددی توسعه داده شده‌اند. با این حال، با توجه به پیچیدگی ذاتی طراحی برخی از این سیستم‌ها از یک طرف و حساسیت موضوع از طرف دیگر، وارسی صحت طراحی و پیاده‌سازی این سیستم‌ها از اهمیت زیادی برخوردار است.بررسی مدل، روشی خودکار برای وارسی سیستم‌های همروند حالت متناهی است و مزایایی نسبت به رهیافت‌های دیگر، مانند شبیه‌سازی، آزمون و استدلال استنتاجی دارد.این روش در عمل به صورت موفق برای وارسی طراحی مدارهای ترتیبی پیچیده و پروتکل‌های ارتباطی استفاده شده است. با توجه به ویژگی خودکار بودنفرایند بررسی مدل، این روش می‌تواند در کنار ابزارهای آن، برای مدل‌سازی و وارسی سیستم‌های کنترل حمل و نقل که ویژگی‌های ایمنی و عاقبت به خیری در آنها ضرورت دارند، به صورت کارآمد استفاده شود. در این مقاله، کنترل‌کننده‌‌یترافیک یک تقاطع را به عنوان یک کاربرد عملی، مدل‌سازی کرده،سپس خواص مورد انتظار این سیستم را با ارائه‌ی فرمول‌های منطق زمانی CTLبا استفاده از ابزار بررسی مدل نمادین NuSMVوارسی می‌کنیم. نتایج حاصل از پیاد‌ه‌سازی و وارسی مدل کنترل ترافیک (به عنوان یک کاربرد نمونه)، اهمیت استفاده از روش بررسی مدل در کاربردهایی مشابه و اقتضائات آنها را نشان می‌دهد.

By MDSERG Admin | مقالات فارسی
DETAIL

تماس با ما

رایانامه: Zamani[AT]eng.ui.ac.ir
شماره تماس: 37934537-31-98+
آدرس: خیابان هزارجریب، دانشگاه اصفهان، دانشکده مهندسی نرم افزار

Statistics

  • 0
  • 0
  • 18
  • 7,282
  • 310
  • 74
  • 0
  • نوامبر 30, 2018
TOP