روشی برای تایید خودکار تبدیل های نمودار تصادفی

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

کلیدواژه ها:

تبدیل نمودار ، بررسی مدل تصادفی ، زنجیره مارکوف ، زمان پیوسته