اعتبارسنجی پروتکل ارسال پیام در یک سیستم توزیعی زمانی

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

کلیدواژه ها:

ارتباطات پیامی ، پروتکل دقیقا یکبار ، سیستمهای توزیع شده ، ماشین زماندار ، وارسی مدل