محاسبه دقیق مقدار ویژگی دسترس پذیری به کمک سیستم های تبدیل گراف

در طراحی های فرمال صورت گرفته، وقوع و یا عدم وقوع یک اتفاق گارانتی شده، طراح با اطمینانطراحی خود را به پایان می برد. از جمله سیستم های فرمال می توان به سیستم های تبدیل گرافاشاره کرد. در پیاده سازی این سیستم به کمک ابزار GROOVE با ترسیم کل فضای حالت بهصورت خودکار، ویژگیهایی همچون وقوع حتمی یک اتفاق، ایمنی (عدم وقوع حتمی یکاتفاق)، دسترس پذیری (احتمال وقوع یک رویداد) و وقوع یک اتفاق در تمام حالات به کمکCTL قابل محاسبه است. نقصانی که در این میان وجود دارد صفر و یک بودن تحلیل است. درحالات ذکر شده سه حالت فاقد مشکل بود و صفر یا یک است مثلا وقوع حتمی یک حالت یعنی بهاحتمال 100 درصد و عدم وقوع آن یعنی به احتمال 0 درصد یک اتفاق حادث گردد، در حالی کهدر دسترس پذیری امکان وقوع یک رویداد وجود داشته و درصد احتمال آن دقیقا مشخص نیست.در واقع وقوع زیر یک درصد و بالای 99 درصد از دید سیستم به یک شکل بیان می شود. حال اگرمواردی وجود داشته باشد که درآنها میزان این احتمال درخور اهمیت باشد از آنجایی که ابزارGROOVE به صورت مستقیم فاقد این قابلیت بوده در این مقاله میزان دقیق احتمال وقوع هرحالات محاسبه و رویکردی جدید در کاربا سیستم تبدیل گراف ارائه گردیده است.

کلیدواژه ها:

سیستم تبدیل گراف ، دسترس پذیری ، PROLOG ، GROOVE