سیدمرتضی بابامیر - دانشگاه کاشان-گروه مهندسی کامپیوتر
سعید جلیلی - دانشگاه تربیت مدرس-گروه مهندسی کامپیوتر

ما در این مقاله رویکردی مبتنی بر منطق حساب رخداد را برای وارسی پویای سیستمهای توزیعشده، شامل رفتار پردازهها و ارتباطات بین آنها، ارائه میدهیم وسپس با طرح مسئله وارسی پروتکل ارتباطات پیامی مطمئن چگونگی استفاده از رویکردمان را در حل آن نشان میدهیم. در این رویکرد رفتار مطلوب پردازهها و ارتباطات مطمئن را با منطق حساب رخداد توصیف میکنیم و سپس نشان میدهیم که چگونه از آنها برای وارسی پویای(زمان اجرای) سیستم بهره بگیریم. رویکرد ما شامل 4 قدم است: ( 1)استفاده از روش رسمی سبک و جدولیSCR برای توصیف رفتار مطلوب پردازههای فرستنده و گیرنده و سپس ارائه طریقی برای استخراج مجموعه قوانین منطقی حساب رخداد از آنها. از این مجموعه قوانین مرجع، برای وارسی اجرای پردازهها به صورت استدلال قیاسی در قدم سوم استفاده میکنیم، 2) بیان ویژگیهای ارتباطات پیامی مطمئن بر حسب فرمولهای حساب رخداد، ( 3) تفسیر این فرمولها با عنایت به قوانین مرجع(یعنی قوانین توصیف رفتار ) مطلوب) و استحصال گزارههای وارسی از روی آنها و ( 4) پایش و وارسی رفتار حین اجرای برنامهها به وسیله گزارههای وارسی.

وارسی پویا، توصیف جدولی، حساب رخداد، ارتباطات پیامی، سیستم توزیعشده