وارسی ویژگی های Liveness در سیستم های بازنویسی عبارات با استفاده از ماشین های درختی متناهی و تحلیل پایان پذیری

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

کلیدواژه ها:

پایان پذیری ، سیستم های بازنویسی عبارات ، ماشین های درختی متناهی ، ویژگی های Liveness