علی خلیلی - دانشکده مهندسی کامپیوتر، دانشگاه علم و صنعت ایران
محمد عبداللهی ازگمی - دانشکده مهندسی کامپیوتر، دانشگاه علم و صنعت ایران

روش های صوری یکی از ابزارهای تحلیل سیستم ها هستند. این روش ها می توانند در شبکه های حسگر بی سیم که از جهات زیادی با شبکه های سنتی متفاوتند نیز اعمال شوند. شبکه های پتری رنگی که بسط شبکه های پتری هستند، از قوی ترین مدل های صوری به شمار می روند. در این مقاله به مدل سازی و ارزیابی کارایی یک پروتکل کنترل دسترسی به رسانه به نام S-MAC در شبکه های حسگر بی سیم با استفاده از شبکه های پتری رنگی پرداخته شده است. پروتکل S-MAC یک پروتکل با اتلاف انرژی محدود و با زمان بندی خواب و بیداری است. در مدل سازی این پروتکل، برای مدل سازی شبکه، از قابلیت سلسه مراتبی موجود در شبکه های پتری رنگ استفاده شده است. استفاده از این روش و چگونگی مدل کردن انتقالات پخشی، می تواند مبنایی برای مدل کردن دیگر پروتکل های لایه کنترل دسترسی به رسانه در شبکه های حسگر بی سیم یا شبکه های متحرک موردی باشد.

پروتکل کنترل دسترسی به رسانه، شبکه های پتری رنگی، شبکه های حسگر بی سیم، مدل سازی صوری