سیده سارا شریفی راد - کارشناس ارشد مهندسی نرم افزار
سیده مریم شریفی راد

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

سیستم های همروند، بن بست، روشهای صوری، توصیف صوری، زبان z