راست آزمایی قابلیت ایمنی الگوریتم باکری با زبان برنامه نویسی با محدودیت مینی زینک

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

کلیدواژه ها:

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