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

روشهای صوری و فنون درستی یابی، از ابزارهای تحلیل سیستم ها هستند. این روشها می توانند در مدل سازی شبکه های حسگر بی سیم که از جهات زیادی با شبکه های سنتی متفاوتند نیز به کار روند. ما در این مقاله، به درستی یابی احتمالی یک سیستم نمونه در شبکه های حسگر بی سیم خواهیم پرداخت. هدف این سیستم، تشخیص رخدادهای مورد نظر در محدوده شبکه است. در این راستا، در ابتدا یک مدل پایه برای شبکه مطرح شده وسپس با حذف بعضی پیش فرض ها سعی خواهد شد تا رفتار مدل به یک سیستم واقعی نزدیکتر شود. برای تحلیل و بررسی سیستم از ابزار درستی یابی احتمالی PRISM استفاده شده و با استفاده از مدل پاداش موجود در این ابزار و استفاده از درستی یابی احتمالی، بعضی از خصوصیت های شبکه به طور نمونه درستی یاب شده است.

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